{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003928499,0.002144016,0.001340002,0.001406935,0.001225813,0.003960912,0.003279794,0.003326647,0.02973611],"category_scores_gemma":[0.01628278,0.001050213,0.002644545,0.002369453,0.002227647,0.01377627,0.003449769,0.005848985,0.005825638],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002887485,"about_ca_system_score_gemma":0.00262616,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001662766,"about_ca_topic_score_gemma":0.002542292,"domain_scores_codex":[0.9935048,0.001187216,0.000364182,0.001560737,0.002227997,0.001155097],"domain_scores_gemma":[0.9872963,0.007724205,0.0004888545,0.003432638,0.0007807955,0.0002771537],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.002486635,0.0008524176,0.002236558,0.002170858,0.000231268,0.0006029153,0.000509236,0.07881025,0.06091848,0.3454887,0.061892,0.4438007],"study_design_scores_gemma":[0.0005220829,0.0003258144,0.0009639492,0.0002322875,0.0002116616,0.001368892,0.0003316258,0.4233636,0.03722343,0.4940577,0.04133477,0.00006417545],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.08143615,0.006616788,0.8123696,0.02332962,0.001196078,0.0003354882,0.00190191,0.01049993,0.06231441],"genre_scores_gemma":[0.3931162,0.002932079,0.579157,0.003098848,0.0008932293,0.0003934788,0.001813278,0.001854585,0.01674135],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02973611,"threshold_uncertainty_score":0.09947717,"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."}}