{"id":"W2294843272","doi":"10.1007/978-3-662-48899-7_29","title":"Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination","year":2015,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":30,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Preprocessor; Computer science; True quantified Boolean formula; Cube (algebra); Algorithm; Solver; Power (physics); Artificial intelligence; Mathematics; Combinatorics; 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.003634275,0.0005717751,0.000504361,0.001062346,0.000333934,0.0006681792,0.003954634,0.0004489359,0.00001586166],"category_scores_gemma":[0.0004386317,0.0005769636,0.0001133648,0.0008847741,0.0007353115,0.001089329,0.001005351,0.001091327,0.00006458371],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001206059,"about_ca_system_score_gemma":0.001089794,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002715722,"about_ca_topic_score_gemma":0.00007050759,"domain_scores_codex":[0.9947717,0.0001419886,0.0007062847,0.001710983,0.001828026,0.0008410675],"domain_scores_gemma":[0.996323,0.0005149729,0.0004102445,0.001800837,0.0006825892,0.0002683733],"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.00001403352,0.00005931097,0.000009710418,0.0001111519,0.00001166767,0.00002784427,0.001264445,0.0570437,0.01057961,0.01721487,0.00006770543,0.913596],"study_design_scores_gemma":[0.0002680456,0.000190258,0.00003846438,0.0003382745,0.000007756089,0.00002105394,3.324148e-7,0.9509478,0.022862,0.02383505,0.0008517732,0.0006391767],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0001660145,0.0005406668,0.9951211,0.0006201362,0.001740742,0.0005009387,0.00000731462,0.0002978726,0.001005189],"genre_scores_gemma":[0.08381505,0.00001867249,0.9150716,0.000514593,0.0001567681,0.00001427779,0.00002030847,0.0000473925,0.0003413331],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9129568,"threshold_uncertainty_score":0.9996682,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02872134792203278,"score_gpt":0.2991227532607629,"score_spread":0.2704014053387301,"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."}}