{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001375846,0.0008187578,0.0007932074,0.0009722007,0.000550577,0.001237266,0.001360713,0.0009378202,0.003807965],"category_scores_gemma":[0.003395852,0.0006985695,0.001063487,0.001301101,0.0009289228,0.002860244,0.002002674,0.001830398,0.0007590269],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001115109,"about_ca_system_score_gemma":0.001974423,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003179837,"about_ca_topic_score_gemma":0.00755591,"domain_scores_codex":[0.998973,0.0004575474,0.0000495071,0.0001721323,0.0002217212,0.0001260293],"domain_scores_gemma":[0.9979037,0.001224637,0.0001784008,0.0003275699,0.0002577219,0.0001080049],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0003625393,0.0003656604,0.002029649,0.0003632664,0.0001170119,0.0002795604,0.0004408706,0.6200188,0.02313685,0.09144805,0.007781016,0.2536567],"study_design_scores_gemma":[0.00005373068,0.00002936994,0.0001269677,0.00001540195,0.00001781397,0.00003725409,0.0000666642,0.9539632,0.006028622,0.03599068,0.003660379,0.00000999706],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02414397,0.0001600395,0.9705989,0.0002834097,0.00002433519,0.0001108327,0.0001055371,0.001011503,0.003561438],"genre_scores_gemma":[0.2023691,0.0002493993,0.7928234,0.0001903525,0.00002714772,0.000308596,0.0006208054,0.000271239,0.003139841],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.003807965,"threshold_uncertainty_score":0.01273888,"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."}}