{"id":"W2914871854","doi":"10.1007/11889205_37","title":"Preprocessing QBF","year":2006,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":45,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Preprocessor; Computer science; True quantified Boolean formula; Expressive power; Solver; Algorithm; Conjunctive normal form; Time complexity; Range (aeronautics); Theoretical computer science; Artificial intelligence; 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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.00144223,0.0004696917,0.0004208464,0.0007629995,0.0002840602,0.0007517214,0.004157543,0.0003458129,0.00001258061],"category_scores_gemma":[0.0001472279,0.0004484482,0.000106175,0.0007260568,0.0006784965,0.001128672,0.001215779,0.0007712891,0.00006886674],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003553533,"about_ca_system_score_gemma":0.0005164993,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002104881,"about_ca_topic_score_gemma":0.00001323983,"domain_scores_codex":[0.9959888,0.00004149508,0.0005790206,0.001703606,0.001055824,0.0006312623],"domain_scores_gemma":[0.9970879,0.0002336511,0.0003940312,0.001901502,0.0002634433,0.0001194551],"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.00000226775,0.00001931661,0.00003221057,0.00005238987,0.000003533445,0.00002907631,0.0002883191,0.03901884,0.0001575327,0.04025629,0.00004766207,0.9200926],"study_design_scores_gemma":[0.0001328477,0.00007625121,0.0001842669,0.0003254267,0.000005082847,0.00007224616,3.519851e-8,0.7501922,0.004403289,0.2401361,0.003815228,0.0006570044],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0000207821,0.0004399008,0.9716552,0.0002156964,0.001814159,0.0002800546,0.000001747017,0.0002882439,0.02528423],"genre_scores_gemma":[0.01660917,0.00001224518,0.9813658,0.0006094092,0.0004602597,0.000009054794,0.000003411484,0.00003207658,0.0008985667],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9194356,"threshold_uncertainty_score":0.9997967,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02513833083533195,"score_gpt":0.2811366149434357,"score_spread":0.2559982841081038,"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."}}