{"id":"W129935311","doi":"10.1609/aaai.v24i1.7548","title":"Exploiting QBF Duality on a Circuit Representation","year":2010,"lang":"en","type":"article","venue":"Proceedings of the AAAI Conference on Artificial Intelligence","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":33,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Unit cube; Representation (politics); Cube (algebra); Duality (order theory); Dual (grammatical number); Solver; Computer science; Unit (ring theory); Value (mathematics); Truth value; Conjunctive normal form; Algorithm; Theoretical computer science; Mathematics; Discrete mathematics; Combinatorics; Programming language; Machine learning; Law; Linguistics","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.001343067,0.0001947272,0.00020742,0.0001351711,0.0002510083,0.0002998349,0.002142686,0.0001140958,0.00006422895],"category_scores_gemma":[0.002334548,0.0001557646,0.0001089634,0.0007366488,0.0002561076,0.0008860113,0.0002884179,0.0005780905,0.0001294496],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003581518,"about_ca_system_score_gemma":0.00006854283,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000397054,"about_ca_topic_score_gemma":0.00000600779,"domain_scores_codex":[0.9978263,0.00004058645,0.0005974455,0.0005797395,0.0006467889,0.0003091534],"domain_scores_gemma":[0.997929,0.0001652471,0.0005578251,0.000600131,0.0006610538,0.00008677607],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00001909748,0.00007643685,0.0001435234,0.00001505355,0.000003900504,1.395126e-7,0.001024659,0.0000138054,0.1507124,0.7586101,0.00002480069,0.08935607],"study_design_scores_gemma":[0.0000151175,0.00009259407,0.0006409212,0.00006305756,0.000003680802,0.000003745764,0.0003004167,0.03196692,0.6834587,0.2832363,0.00007822285,0.0001402103],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.6776385,0.000003318019,0.2553908,0.003070598,0.002103815,0.0007511448,0.000005143238,0.0002843696,0.06075228],"genre_scores_gemma":[0.9679349,0.000005764371,0.03151432,0.00021523,0.0001148759,0.00004512757,3.681725e-7,0.00001105771,0.0001583689],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.5327463,"threshold_uncertainty_score":0.6351897,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1997012440612117,"score_gpt":0.3678475354696475,"score_spread":0.1681462914084358,"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."}}