{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.000326145,0.00004099179,0.00003769272,0.00003752556,0.00005290968,0.0000542025,0.0003995096,0.00001870534,0.00003969212],"category_scores_gemma":[0.00004200529,0.00003453034,0.00001888085,0.0001481593,0.00001208551,0.0001252874,0.0001058456,0.00004108719,0.000576127],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003392596,"about_ca_system_score_gemma":0.00001191216,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000002561015,"about_ca_topic_score_gemma":0.000001045155,"domain_scores_codex":[0.999489,0.00002489669,0.00009426994,0.0001405832,0.0001255347,0.0001257259],"domain_scores_gemma":[0.9995551,0.00002312661,0.00002357251,0.0003398843,0.00002395502,0.00003440658],"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":[5.672106e-7,0.000028859,0.00005546508,0.000002008847,0.000001425017,3.700987e-7,0.0003708861,0.007109679,0.002152144,0.6477829,0.000517752,0.341978],"study_design_scores_gemma":[0.00004517091,0.000008885352,0.001376996,0.000001952721,4.296443e-7,0.000004806655,0.000006136459,0.9743593,0.0129172,0.0002563149,0.01096506,0.00005771353],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01589411,0.00002938232,0.9452835,0.0005294126,0.0001887785,0.00004166805,4.944489e-8,0.0001949419,0.03783811],"genre_scores_gemma":[0.3376948,4.901126e-7,0.661557,0.0002587348,0.00003655949,0.000002077545,7.537603e-8,0.000001483383,0.0004487944],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9672496,"threshold_uncertainty_score":0.7405139,"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."}}