{"id":"W2062671967","doi":"10.1016/j.jcss.2003.07.011","title":"A sharp threshold in proof complexity yields lower bounds for satisfiability search","year":2003,"lang":"en","type":"article","venue":"Journal of Computer and System Sciences","topic":"Constraint Satisfaction and Optimization","field":"Computer Science","cited_by":61,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Satisfiability; Mathematics; Combinatorics; Resolution (logic); Range (aeronautics); Conjunctive normal form; Discrete mathematics; Exponential function; Boolean satisfiability problem; Upper and lower bounds; Exponential time hypothesis; Time complexity; Computer science","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":[],"consensus_categories":[],"category_scores_codex":[0.002759427,0.00009277017,0.0002426959,0.0002202099,0.0001974216,0.0003853101,0.0003627492,0.00004337002,0.000006060229],"category_scores_gemma":[0.00002711884,0.00006938839,0.00007090343,0.000413275,0.0001858784,0.0006696031,0.00005067446,0.0001150288,4.59658e-7],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005639738,"about_ca_system_score_gemma":0.000233697,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000006736957,"about_ca_topic_score_gemma":0.00002341101,"domain_scores_codex":[0.9985802,0.0001378821,0.0004802995,0.0002261437,0.000374805,0.0002006623],"domain_scores_gemma":[0.9992278,0.000172186,0.000173466,0.0001312547,0.0001988239,0.00009645084],"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.00003993714,0.0002026817,0.1376455,0.0002795901,0.00003029,0.0000273215,0.002595701,0.01375821,0.00008224919,0.8041597,0.0006712522,0.04050759],"study_design_scores_gemma":[0.001193015,0.0009001095,0.05915838,0.0002454585,0.000006208176,0.0006248533,0.0003581636,0.9258829,0.0001780723,0.01070209,0.0005141361,0.0002365623],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1062497,0.0001109933,0.8907408,0.0005283755,0.0007710995,0.0002142312,0.000001136832,0.00001262532,0.00137104],"genre_scores_gemma":[0.9075145,0.000002961602,0.09234968,0.00006916552,0.00005107039,0.000002389114,8.160926e-8,0.000001778276,0.000008367743],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9121248,"threshold_uncertainty_score":0.3715554,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05440909133257375,"score_gpt":0.293218237044864,"score_spread":0.2388091457122902,"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."}}