{"id":"W2105210717","doi":"10.1109/ictai.2004.67","title":"Guiding real-world SAT solving with dynamic hypergraph separator decomposition","year":2005,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":35,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Satisfiability; Solver; Hypergraph; Preprocessor; Computer science; Decomposition; Boolean satisfiability problem; Mathematical optimization; Theoretical computer science; Algorithm; Parallel computing; Mathematics; Discrete mathematics; Artificial intelligence","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.0004136782,0.0001312806,0.0001200789,0.0002030797,0.0001807027,0.0001580894,0.0005084433,0.00003691292,0.00002258082],"category_scores_gemma":[0.00001222977,0.000109304,0.00003808001,0.0006192665,0.0000323358,0.001183527,0.00009219228,0.00007044458,0.0001063859],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001553718,"about_ca_system_score_gemma":0.00003715457,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004021177,"about_ca_topic_score_gemma":0.0002854567,"domain_scores_codex":[0.9988631,0.00007542001,0.0002288213,0.0003403538,0.0002327213,0.0002596108],"domain_scores_gemma":[0.9991636,0.00005220749,0.00009644277,0.0005340175,0.00007466236,0.00007905154],"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.00004804158,0.0001635677,0.005088072,0.00003654322,0.0000571906,0.000009061514,0.001005304,0.004754308,0.07897057,0.6915391,0.001404173,0.216924],"study_design_scores_gemma":[0.0002845723,0.00009897909,0.01429878,0.00004503691,0.00001031708,0.00003220712,0.00002513063,0.9464968,0.03354567,0.0008853613,0.003934523,0.0003425848],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.08025748,0.00003230586,0.8926819,0.0004517153,0.0001527097,0.0001306001,4.415181e-7,0.0003950231,0.02589784],"genre_scores_gemma":[0.4287454,0.00001062466,0.5706133,0.0001783866,0.00003022414,0.000009682269,0.000002016282,0.000006921102,0.0004034884],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9417425,"threshold_uncertainty_score":0.4457289,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0225522952811187,"score_gpt":0.3226581852749304,"score_spread":0.3001058899938117,"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."}}