{"id":"W2955759369","doi":"10.1007/978-3-030-24258-9_11","title":"Speeding Up Assumption-Based SAT","year":2019,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Solver; Boolean satisfiability problem; Maximum satisfiability problem; Simple (philosophy); Satisfiability; Conjunctive normal form; Propositional calculus; Propositional formula; Algorithm; Forcing (mathematics); Theoretical computer science; Mathematical optimization; Programming language; Mathematics; Boolean function; Propositional variable; Description logic","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.003402238,0.002083961,0.001994231,0.001771196,0.001475609,0.003063789,0.00651891,0.001869643,0.06644935],"category_scores_gemma":[0.01915183,0.001815021,0.003109647,0.002935126,0.002077292,0.01047136,0.007785659,0.006161013,0.01358566],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002479221,"about_ca_system_score_gemma":0.004009324,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004718844,"about_ca_topic_score_gemma":0.01225895,"domain_scores_codex":[0.9939163,0.001955965,0.0003131129,0.001179274,0.001765412,0.000869895],"domain_scores_gemma":[0.9755287,0.01569346,0.0004920302,0.00655787,0.001396316,0.0003316321],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.002437851,0.0007130272,0.001884971,0.001197434,0.0003566032,0.0002699592,0.0003818114,0.1349563,0.01393451,0.1311497,0.07506464,0.6376531],"study_design_scores_gemma":[0.0004779697,0.0001991296,0.0004438946,0.000104789,0.0001808966,0.0001434163,0.000183019,0.7724031,0.01086969,0.1942668,0.02068789,0.00003939732],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.03695562,0.001068151,0.8807577,0.001910127,0.001193254,0.0005616079,0.001632875,0.03369369,0.04222699],"genre_scores_gemma":[0.3307991,0.0004897741,0.6359962,0.001227182,0.0003510983,0.0006666895,0.004145125,0.003691317,0.02263364],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.06644935,"threshold_uncertainty_score":0.2222952,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03911111324943266,"score_gpt":0.291996833086991,"score_spread":0.2528857198375583,"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."}}