{"id":"W1581900214","doi":"10.1007/11814948_33","title":"Binary Clause Reasoning in QBF","year":2006,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":42,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"DPLL algorithm; Computer science; Binary number; Binary decision diagram; Boolean satisfiability problem; Fragment (logic); True quantified Boolean formula; Resolution (logic); Context (archaeology); Inference; Binary tree; Theoretical computer science; Algorithm; Mathematics; Artificial intelligence; Arithmetic","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"],"consensus_categories":[],"category_scores_codex":[0.001969372,0.0005191091,0.0005158443,0.001440099,0.0001820454,0.0004505457,0.004045402,0.0004371758,0.00001185286],"category_scores_gemma":[0.0001983778,0.0005160744,0.0001049331,0.001208736,0.000598965,0.001095476,0.001369624,0.001166975,0.00005681738],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005908757,"about_ca_system_score_gemma":0.0004648504,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000949664,"about_ca_topic_score_gemma":0.00007795696,"domain_scores_codex":[0.9957626,0.00008976895,0.0007067528,0.001677214,0.0009872895,0.0007763183],"domain_scores_gemma":[0.9971628,0.000345255,0.0003562792,0.001850855,0.0001600721,0.0001247369],"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.00001040834,0.00006426463,0.0004218141,0.00006106114,0.000005508995,0.0002707292,0.0007374459,0.1431222,0.0003112184,0.1106752,0.0001130362,0.7442071],"study_design_scores_gemma":[0.0002535584,0.0001398909,0.001752763,0.0005941114,0.000003628913,0.00007367902,9.919585e-8,0.9039777,0.001165298,0.08889745,0.002387031,0.0007548216],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0002483788,0.0004658672,0.9860066,0.0002634303,0.001903169,0.0003630889,0.000002310507,0.0001985564,0.01054859],"genre_scores_gemma":[0.03080356,0.00003350657,0.9677159,0.0006112432,0.0003189904,0.00001365052,0.000005596347,0.00003609739,0.0004614253],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7608555,"threshold_uncertainty_score":0.9997291,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02207398825870749,"score_gpt":0.2750306988911787,"score_spread":0.2529567106324712,"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."}}