{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001731694,0.0007495189,0.0008214074,0.001294056,0.001311422,0.002199242,0.001932619,0.001352091,0.004146629],"category_scores_gemma":[0.007989396,0.0007348155,0.002196112,0.002243059,0.003131223,0.005186194,0.00305177,0.004362264,0.0006676291],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002158779,"about_ca_system_score_gemma":0.001126995,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004196635,"about_ca_topic_score_gemma":0.003550898,"domain_scores_codex":[0.9980727,0.0007631331,0.0001080877,0.0004243799,0.0004592736,0.0001723939],"domain_scores_gemma":[0.994584,0.004178937,0.0002270668,0.0005105322,0.0003462267,0.0001532089],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0000490771,0.00004166875,0.0004670973,0.0001954159,0.00004383404,0.0001751976,0.0004054369,0.02377682,0.001840849,0.9316556,0.003031252,0.03831784],"study_design_scores_gemma":[0.00002113389,0.00003311657,0.0001516346,0.00003714873,0.00002750954,0.0001962548,0.00009227719,0.1076602,0.001651937,0.8788038,0.01131141,0.00001363467],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02448878,0.002121922,0.9405283,0.004094281,0.0001926545,0.00009257108,0.0002222336,0.0004229929,0.02783625],"genre_scores_gemma":[0.4203166,0.002659146,0.564643,0.001032072,0.0005104275,0.0002418767,0.0005399596,0.0002016172,0.009855289],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.004196635,"threshold_uncertainty_score":0.01566309,"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."}}