{"id":"W1489227721","doi":"10.1109/ccc.2000.856741","title":"An application of matroid theory to the SAT problem","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Matroid; Combinatorics; Decidability; Mathematics; Conjunctive normal form; Discrete mathematics; Constant (computer programming); Matching (statistics); Resolution (logic); Time complexity; Computer science","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0007387187,0.00004434359,0.00004677587,0.00003362277,0.00004781715,0.00003115403,0.0008704184,0.00002002561,0.00002711743],"category_scores_gemma":[0.00001930969,0.00002818043,0.0000161865,0.0002815297,0.00002119386,0.0002576075,0.0000635765,0.00003693024,0.0002104399],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001203584,"about_ca_system_score_gemma":0.000003382184,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000006801321,"about_ca_topic_score_gemma":0.000002581161,"domain_scores_codex":[0.9993805,0.0001158617,0.0001307313,0.0001529106,0.0001320883,0.00008795768],"domain_scores_gemma":[0.9990323,0.00003692727,0.00005211206,0.000799493,0.00004647349,0.00003268734],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000001123027,0.0000233772,0.00005234587,0.000002832443,0.000001053903,1.662729e-8,0.0005619241,0.0001762375,0.004429184,0.723497,0.000225263,0.2710297],"study_design_scores_gemma":[0.0001193659,0.0002501368,0.006534018,0.000006085728,0.000005015374,0.000009350639,0.0001348266,0.8505267,0.048626,0.06588067,0.02771815,0.0001897179],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.002282584,0.00001906976,0.9862977,0.000773697,0.00004218152,0.0002667194,4.004076e-7,0.00008511748,0.01023254],"genre_scores_gemma":[0.3442705,0.000001490022,0.6552042,0.0002670725,0.00001663697,0.00003697878,2.990122e-7,0.000002380057,0.0002004156],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8503504,"threshold_uncertainty_score":0.2704849,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02140411412129907,"score_gpt":0.2820081663074063,"score_spread":0.2606040521861073,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}