{"id":"W2036901448","doi":"10.1007/978-3-642-02777-2_38","title":"Beyond CNF: A Circuit-Based QBF Solver","year":2009,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":31,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Conjunctive normal form; Boolean satisfiability problem; Computer science; True quantified Boolean formula; Solver; Satisfiability; Representation (politics); Theoretical computer science; DPLL algorithm; Algorithm; Programming language","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":["metaepi_narrow","open_science"],"consensus_categories":[],"category_scores_codex":[0.001809582,0.0006797721,0.0006197993,0.001133968,0.0003228488,0.000704436,0.005551145,0.000519371,0.00003955442],"category_scores_gemma":[0.0001986306,0.000654825,0.0002119912,0.0009825835,0.0008152305,0.0009576813,0.0007217174,0.001125677,0.0001270926],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005124652,"about_ca_system_score_gemma":0.0009055677,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000103393,"about_ca_topic_score_gemma":0.00001820007,"domain_scores_codex":[0.9947873,0.00007836214,0.0007083885,0.001999937,0.001513727,0.0009122446],"domain_scores_gemma":[0.9959344,0.0004131323,0.0004446367,0.002615563,0.0003357071,0.0002565391],"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.000004096127,0.00003303937,0.00001329163,0.00002539168,0.000005015608,0.00003654881,0.0002498685,0.01581437,0.0001995779,0.1073663,0.00003174989,0.8762208],"study_design_scores_gemma":[0.0002875059,0.0002445448,0.0002377492,0.0002293874,0.000008925521,0.00004580901,4.452473e-8,0.5892451,0.003582102,0.4010143,0.004261038,0.0008434908],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00001252461,0.0003728002,0.9739056,0.0005782269,0.002393125,0.0004677121,0.00000451092,0.0003277494,0.0219378],"genre_scores_gemma":[0.01618419,0.00001551782,0.9785078,0.004226346,0.0005023049,0.00001261922,0.000006771335,0.00003973309,0.0005047168],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8753772,"threshold_uncertainty_score":0.9998293,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02784531932557335,"score_gpt":0.2694459329565025,"score_spread":0.2416006136309292,"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."}}