{"id":"W6986608131","doi":"","title":"Prioritized Unit Propagation and Extended Resolution Techniques for SAT Solvers","year":2023,"lang":"en","type":"dissertation","venue":"UWSpace (University of Waterloo)","topic":"Constraint Satisfaction and Optimization","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Blackberry (Canada)","funders":"","keywords":"Heuristics; Boolean satisfiability problem; Maximum satisfiability problem; Heuristic; Resolution (logic); Satisfiability; Class (philosophy); Constraint (computer-aided design); True quantified Boolean formula","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.0001946246,0.0001569149,0.0002254968,0.0003962987,0.0002582702,0.00005404092,0.0002421346,0.0002329079,0.00001257406],"category_scores_gemma":[0.00002860128,0.0001947377,0.00008604593,0.0002784581,0.00006016549,0.0004485421,0.00005510421,0.0001172048,0.000007657577],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00006404413,"about_ca_system_score_gemma":0.0001161497,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001912247,"about_ca_topic_score_gemma":0.01165336,"domain_scores_codex":[0.9990886,0.00004571511,0.000125755,0.000370903,0.0001979755,0.0001710648],"domain_scores_gemma":[0.9991463,0.00004954883,0.0002424325,0.0002228755,0.000279195,0.00005962293],"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.001055132,0.0001922477,0.0006666807,0.002368407,0.0003505618,0.00004140956,0.2169441,0.0002016864,0.03449237,0.03471234,0.006440897,0.7025342],"study_design_scores_gemma":[0.01207926,0.00239248,0.1576483,0.003407116,0.00114685,0.00004609858,0.3669589,0.3831277,0.03866256,0.01976229,0.009850517,0.00491797],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"other","genre_scores_codex":[0.5680653,0.0001177212,0.4182577,0.004346704,0.001632757,0.004242748,0.0001155947,0.002239507,0.000981995],"genre_scores_gemma":[0.07897591,0.00107379,0.3715355,0.00005031538,0.0001073361,0.00001686625,0.003046134,0.00008768074,0.5451065],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6976162,"threshold_uncertainty_score":0.7941173,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01425772118000953,"score_gpt":0.2274240442898645,"score_spread":0.213166323109855,"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."}}