{"id":"W4239560685","doi":"10.1109/dac.2005.193910","title":"Efficient SAT solving: beyond supercubes","year":2005,"lang":"en","type":"article","venue":"Proceedings. 42nd Design Automation Conference, 2005.","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":"Pruning; Computer science; Speedup; Boolean satisfiability problem; Benchmark (surveying); Maximum satisfiability problem; Solver; Theoretical computer science; Boolean function; Algorithm; Programming language; Parallel computing","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.002055059,0.0006999183,0.001431388,0.0009653603,0.001079867,0.002169469,0.002679971,0.001136706,0.006050116],"category_scores_gemma":[0.007588911,0.0007568088,0.001182851,0.002273882,0.001633771,0.005278199,0.003306476,0.00256796,0.001529633],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001318606,"about_ca_system_score_gemma":0.001872133,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.005783648,"about_ca_topic_score_gemma":0.008262059,"domain_scores_codex":[0.9966208,0.001296929,0.0001820109,0.0004361377,0.001167606,0.0002964517],"domain_scores_gemma":[0.9953377,0.002188921,0.0001869471,0.001628775,0.0005416753,0.0001158589],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0002577287,0.0001837546,0.001383388,0.0005081684,0.0001132021,0.0001848818,0.0004316479,0.1518528,0.009126751,0.3568578,0.01763866,0.4614612],"study_design_scores_gemma":[0.00007895636,0.0000743297,0.0002699512,0.00008341585,0.00003600834,0.000111432,0.0001657608,0.691431,0.006474548,0.2671984,0.03405741,0.00001875779],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02913886,0.001623623,0.9478704,0.001721998,0.000121224,0.0001740951,0.0001855857,0.002026593,0.01713768],"genre_scores_gemma":[0.1743639,0.001309559,0.8175706,0.0006721506,0.000096264,0.0003437829,0.0006535323,0.0006567694,0.004333389],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006050116,"threshold_uncertainty_score":0.02023965,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04063998466356675,"score_gpt":0.274707702467188,"score_spread":0.2340677178036212,"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."}}