{"id":"W2162493591","doi":"10.1145/1065579.1065774","title":"Efficient SAT solving","year":2005,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"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.001585241,0.001222275,0.001224034,0.001439321,0.001161101,0.002388129,0.002247519,0.00125149,0.0240766],"category_scores_gemma":[0.007461336,0.0007733547,0.00183043,0.002012605,0.000822645,0.002911937,0.002397306,0.00228386,0.006139308],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001575001,"about_ca_system_score_gemma":0.002489139,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003105518,"about_ca_topic_score_gemma":0.00693082,"domain_scores_codex":[0.9967657,0.001031139,0.0001953216,0.0005440933,0.001047665,0.0004160597],"domain_scores_gemma":[0.9969082,0.001523001,0.0001193154,0.000878553,0.0005046467,0.00006631415],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0001916395,0.0003093343,0.001271187,0.0008947669,0.000219656,0.0002493151,0.0002377656,0.1370557,0.01379538,0.2319747,0.04738007,0.5664205],"study_design_scores_gemma":[0.0001943336,0.000104088,0.0005742829,0.0001292151,0.000113264,0.0002928326,0.0002787384,0.6074497,0.01750838,0.2894872,0.08383291,0.00003508203],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01638629,0.001113561,0.9319447,0.001387019,0.0002118097,0.0003494544,0.0008488754,0.005593878,0.04216441],"genre_scores_gemma":[0.1532176,0.001227194,0.8303786,0.0004698975,0.0001301949,0.000426634,0.003027085,0.0007962117,0.01032663],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.0240766,"threshold_uncertainty_score":0.08054429,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02426087188872086,"score_gpt":0.2889960319657439,"score_spread":0.264735160077023,"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."}}