{"id":"W39832950","doi":"","title":"An Exponential Time/Space Speedup For Resolution","year":2007,"lang":"en","type":"article","venue":"Electronic colloquium on computational complexity","topic":"Logic, Reasoning, and Knowledge","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Resolution (logic); DPLL algorithm; Satisfiability; Speedup; Heuristics; Bottleneck; PSPACE; Mathematical proof; Heuristic; Proof complexity; Space (punctuation); Computer science; Mathematics; Algorithm; Conjunctive normal form; Automated theorem proving; Exponential function; Discrete mathematics; Computational complexity theory; Mathematical optimization; Parallel computing; 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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001449508,0.000292998,0.0002981497,0.0002413652,0.0006475627,0.0002094748,0.0009665125,0.0001156956,0.00007522989],"category_scores_gemma":[0.00008648864,0.0003067545,0.0001830346,0.0005851952,0.0001336907,0.0004210347,0.0001276445,0.0002843607,0.0001978608],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005917287,"about_ca_system_score_gemma":0.000540869,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002755483,"about_ca_topic_score_gemma":0.0001745161,"domain_scores_codex":[0.997053,0.0001526874,0.0004025824,0.0007833542,0.0006029007,0.001005428],"domain_scores_gemma":[0.9981406,0.0005442111,0.0001999498,0.0004934194,0.0003849528,0.0002368266],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0003019049,0.0004343207,0.00005310603,0.00001053084,0.00003700155,0.000004521825,0.00029385,0.006876367,0.00108931,0.9838764,0.003786432,0.00323627],"study_design_scores_gemma":[0.001730594,0.001960583,0.00909668,0.00001429643,0.00001499637,0.00004010386,0.00002165523,0.6824703,0.001408452,0.2840766,0.01863533,0.0005304146],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0623721,0.0001177262,0.9306779,0.0006882351,0.0005051348,0.0006042744,0.00001439048,0.000413134,0.004607088],"genre_scores_gemma":[0.9468746,0.000001620676,0.051411,0.000333288,0.000540793,0.00002664473,0.000149469,0.00002354473,0.000639011],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.8845025,"threshold_uncertainty_score":0.9999384,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02567232214564987,"score_gpt":0.2977253419486561,"score_spread":0.2720530198030063,"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."}}