{"id":"W2052175425","doi":"10.5555/2485288.2485484","title":"Bridging the gap between dual propagation and CNF-based QBF solving","year":2013,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":31,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Bridging (networking); Conjunctive normal form; Expressive power; True quantified Boolean formula; Dual (grammatical number); Solver; Theoretical computer science; Inefficiency; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006623928,0.0007664056,0.0007724687,0.001191899,0.0009726227,0.002515994,0.002514992,0.001328054,0.007709722],"category_scores_gemma":[0.01962223,0.0006548243,0.001014004,0.001436094,0.002480246,0.004251005,0.004182306,0.003668199,0.000914601],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002478117,"about_ca_system_score_gemma":0.003806233,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006254843,"about_ca_topic_score_gemma":0.006135602,"domain_scores_codex":[0.9949908,0.002564247,0.0002657606,0.0004521869,0.001365114,0.0003618938],"domain_scores_gemma":[0.9875608,0.009423958,0.0003808949,0.001213979,0.001237209,0.0001832035],"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.0003369013,0.0003596511,0.0009509415,0.0004629368,0.0000706974,0.0002009337,0.0003980081,0.143872,0.006119047,0.5832133,0.006969376,0.2570462],"study_design_scores_gemma":[0.00004662925,0.00004091327,0.00007329405,0.00005758037,0.00001682002,0.00005837396,0.00004011808,0.8128031,0.005399285,0.1760695,0.00537861,0.00001577446],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.007013439,0.0001884802,0.9856195,0.0006301052,0.00006087537,0.00009027385,0.00004943769,0.0005132524,0.005834553],"genre_scores_gemma":[0.2202002,0.0004645874,0.7740304,0.0005489573,0.00007479983,0.0002427572,0.0002585266,0.000259531,0.003920203],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007709722,"threshold_uncertainty_score":0.03503108,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04456672099006587,"score_gpt":0.2785642733075658,"score_spread":0.2339975523174999,"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."}}