{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0008800668,0.0005044105,0.0005052451,0.0009362493,0.0004297839,0.001542583,0.00112981,0.0007902559,0.005099325],"category_scores_gemma":[0.004449909,0.0003442688,0.0007450865,0.0009746811,0.001307225,0.002818431,0.00165109,0.001944821,0.0007197881],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0009248948,"about_ca_system_score_gemma":0.001045806,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001044982,"about_ca_topic_score_gemma":0.001427435,"domain_scores_codex":[0.9990127,0.0003583885,0.0000430924,0.0001464423,0.0003401811,0.00009924905],"domain_scores_gemma":[0.9986666,0.0007418738,0.00009045737,0.0002700064,0.0001923378,0.00003863657],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.000172461,0.000133136,0.0004588486,0.0001898595,0.00002891374,0.0001859974,0.000149278,0.2019032,0.01420579,0.5835615,0.00313419,0.1958768],"study_design_scores_gemma":[0.0000382155,0.00008134528,0.00008719945,0.00002685528,0.00002625243,0.0001210819,0.00003380537,0.6142397,0.007786989,0.3696545,0.007889878,0.00001420369],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01305846,0.0001047356,0.9804586,0.0003291804,0.00002464951,0.00005822468,0.000120345,0.0005883474,0.005257438],"genre_scores_gemma":[0.4405907,0.0002892066,0.553815,0.0003306199,0.00004880888,0.0002202244,0.0004343477,0.0001640525,0.004106932],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.005099325,"threshold_uncertainty_score":0.01705897,"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."}}