Short proofs are narrow—resolution made simple
From MaRDI portal
Publication:4406287
DOI10.1145/375827.375835zbMath1089.03507OpenAlexW2084384424MaRDI QIDQ4406287
Publication date: 25 June 2003
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/375827.375835
Related Items
From Small Space to Small Width in Resolution ⋮ Narrow Proofs May Be Maximally Long ⋮ Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ The impact of heterogeneity and geometry on the proof complexity of random satisfiability ⋮ Parity Games and Propositional Proofs ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas ⋮ Space characterizations of complexity measures and size-space trade-offs in propositional proof systems ⋮ Constructing Hard Examples for Graph Isomorphism ⋮ An Introduction to Lower Bounds on Resolution Proof Systems ⋮ Lower bounds for QCDCL via formula gauge ⋮ The Complexity of Propositional Proofs ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ Supercritical Space-Width Trade-offs for Resolution ⋮ Proof Complexity of Non-classical Logics ⋮ Propositional proof complexity ⋮ Unnamed Item ⋮ Complexity of translations from resolution to sequent calculus ⋮ Unnamed Item ⋮ LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE ⋮ MaxSAT Resolution and Subcube Sums ⋮ On space and depth in resolution ⋮ On the automatizability of resolution and related propositional proof systems ⋮ Resolution lower bounds for perfect matching principles ⋮ Knowledge Compilation with Empowerment ⋮ Proof complexity of modal resolution ⋮ Many hard examples in exact phase transitions ⋮ On the complexity of resolution with bounded conjunctions ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ A sharp threshold in proof complexity yields lower bounds for satisfiability search ⋮ Data reductions, fixed parameter tractability, and random weighted \(d\)-CNF satisfiability ⋮ Cumulative Space in Black-White Pebbling and Resolution ⋮ Mining Backbone Literals in Incremental SAT ⋮ Unnamed Item ⋮ A note about \(k\)-DNF resolution ⋮ Width versus size in resolution proofs ⋮ Communication Lower Bounds via Critical Block Sensitivity ⋮ Cryptographic hardness of random local functions. Survey ⋮ Relating size and width in variants of Q-resolution ⋮ FRAGMENTS OF APPROXIMATE COUNTING ⋮ Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas ⋮ A general model and thresholds for random constraint satisfaction problems ⋮ Strong ETH and resolution via games and the multiplicity of strategies ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms ⋮ Space Complexity in Polynomial Calculus ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Improving resolution width lower bounds for \(k\)-CNFs with applications to the strong exponential time hypothesis ⋮ A game characterisation of tree-like Q-resolution size ⋮ Resolution lower bounds for the weak functional pigeonhole principle. ⋮ Spanoids---An Abstraction of Spanning Structures, and a Barrier for LCCs ⋮ Expander graphs and their applications ⋮ The complexity of inverting explicit Goldreich's function by DPLL algorithms ⋮ Satisfiability, branch-width and Tseitin tautologies ⋮ Lower bounds for \(k\)-DNF resolution on random 3-CNFs ⋮ Cliques enumeration and tree-like resolution proofs ⋮ On the automatizability of polynomial calculus ⋮ The depth of resolution proofs ⋮ A characterization of tree-like resolution size ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Complexity of Inversion of Explicit Goldreich’s Function by DPLL Algorithms ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ Lower bound techniques for QBF expansion ⋮ On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution ⋮ A combinatorial characterization of resolution width ⋮ Cutting planes and the parameter cutwidth ⋮ The satisfiability threshold for random linear equations ⋮ Partially definable forcing and bounded arithmetic ⋮ On the power of clause-learning SAT solvers as resolution engines ⋮ The treewidth of proofs ⋮ Space proof complexity for random 3-CNFs ⋮ Characterising tree-like Frege proofs for QBF ⋮ Mean-payoff games and propositional proofs ⋮ Resolution Width and Cutting Plane Rank Are Incomparable ⋮ A simplified way of proving trade-off results for resolution ⋮ Unnamed Item ⋮ Resolution with counting: dag-like lower bounds and different moduli ⋮ A Framework for Space Complexity in Algebraic Proof Systems ⋮ Reversible pebble games and the relation between tree-like and general resolution space ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ Convex Relaxations and Integrality Gaps ⋮ Nullstellensatz size-degree trade-offs from reversible pebbling ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ Definable Inapproximability: New Challenges for Duplicator ⋮ A combinatorial characterization of treelike resolution space ⋮ Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Finding a tree structure in a resolution proof is NP-complete ⋮ Spanoids - An Abstraction of Spanning Structures, and a Barrier for LCCs ⋮ Adventures in monotone complexity and TFNP ⋮ Short Proofs Are Hard to Find ⋮ Size-degree trade-offs for sums-of-squares and positivstellensatz proofs ⋮ Sum of squares bounds for the ordering principle ⋮ Random resolution refutations ⋮ On the One-Way Function Candidate Proposed by Goldreich ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ The Lovász Local Lemma and Satisfiability ⋮ Total Space in Resolution ⋮ Random constraint satisfaction: easy generation of hard (satisfiable) instances ⋮ Resolution for Max-SAT ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search ⋮ Combinatorial Problems for Horn Clauses ⋮ Nullstellensatz size-degree trade-offs from reversible pebbling ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Another look at degree lower bounds for polynomial calculus ⋮ Resolution over linear equations modulo two ⋮ Lower bounds for the weak pigeonhole principle and random formulas beyond resolution ⋮ The resolution complexity of random graph \(k\)-colorability ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ Spines of random constraint satisfaction problems: definition and connection with computational complexity ⋮ Reflections on Proof Complexity and Counting Principles ⋮ Proving unsatisfiability of CNFs locally ⋮ Lower bounds for QCDCL via formula gauge ⋮ On the hierarchical community structure of practical Boolean formulas
