{"id":"W2121072219","doi":"10.5555/1870926.1871338","title":"Leveraging dominators for preprocessing QBF","year":2010,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Preprocessor; Conjunctive normal form; Computer science; Very-large-scale integration; Algorithm; True quantified Boolean formula; Computational complexity theory; Time complexity; Theoretical computer science; Artificial intelligence","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.001483221,0.001105307,0.0006811883,0.001032134,0.0009440311,0.001469707,0.001643121,0.0008865986,0.0112863],"category_scores_gemma":[0.00735434,0.000664026,0.001369051,0.001195974,0.001155771,0.002788337,0.001902889,0.002000765,0.002301263],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001076335,"about_ca_system_score_gemma":0.001852297,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002417252,"about_ca_topic_score_gemma":0.003368626,"domain_scores_codex":[0.9982429,0.0006442616,0.0001203105,0.0003655791,0.0003804328,0.0002465894],"domain_scores_gemma":[0.9939098,0.003764852,0.0003263299,0.001292171,0.0006287912,0.00007802581],"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.0006878281,0.0004570142,0.002171104,0.0007835146,0.0001141279,0.0004722963,0.0004605929,0.1585607,0.1012556,0.1166708,0.01372909,0.6046374],"study_design_scores_gemma":[0.0001688376,0.0003315471,0.0006515931,0.0001191943,0.00007162485,0.0003999505,0.0001369925,0.7277992,0.1209638,0.1250694,0.0242261,0.00006182827],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01822006,0.0001454035,0.9735351,0.000338159,0.00002983459,0.0001605553,0.0001294118,0.003019119,0.004422442],"genre_scores_gemma":[0.2485081,0.0002227904,0.7461969,0.0002729131,0.00005151358,0.0002162796,0.0007425568,0.0006724192,0.003116474],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.0112863,"threshold_uncertainty_score":0.03775638,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02575595631419103,"score_gpt":0.3165616450073915,"score_spread":0.2908056886932004,"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."}}