Lower bounds for resolution and cutting plane proofs and monotone computations

DOI10.2307/2275583zbMath0945.03086OpenAlexW2044095368MaRDI QIDQ4372917

Publication date: 17 December 1997

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275583

zbMATH Keywords

arithmetic circuits exponential lower bound length of cutting plane proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Related Items

Monotone simulations of non-monotone proofs., Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes, On the automatizability of resolution and related propositional proof systems, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Proof tree preserving tree interpolation, Interpolation systems for ground proofs in automated deduction: a survey, Interpolation and model checking for nonlinear arithmetic, Proof complexity of modal resolution, The cost of a cycle is a square, Lower bounds for monotone real circuit depth and formula size and tree-like cutting planes, Nondeterministic functions and the existence of optimal proof systems, Feasible Interpolation for QBF Resolution Calculi, Nisan-Wigderson generators in proof systems with forms of interpolation, Craig Interpolation in the Presence of Non-linear Constraints, Satisfiability Modulo Theories, Interpolation and Model Checking, Lower bounds for monotone counting circuits, Optimal length resolution refutations of difference constraint systems, Theoretical challenges towards cutting-plane selection, Randomized feasible interpolation and monotone circuits with a local oracle, Dag-like communication and its applications, Constraint solving for interpolation, Some consequences of cryptographical conjectures for \(S_2^1\) and EF, Lower Bound Techniques for QBF Proof Systems, Space Complexity in Polynomial Calculus, Classes of representable disjoint \textsf{NP}-pairs, Horn Clause Solvers for Program Verification, Unnamed Item, A note on monotone real circuits, SMT-based verification of program changes through summary repair, Unnamed Item, Logical Closure Properties of Propositional Proof Systems, Towards NP-P via proof complexity and search, A game characterisation of tree-like Q-resolution size, Integer feasibility and refutations in UTVPI constraints using bit-scaling, Complexity of optimizing over the integers, Lower bounds on the size of general branch-and-bound trees, Complexity of branch-and-bound and cutting planes in mixed-integer optimization, Exponential lower bounds on the complexity of a class of dynamic programs for combinatorial optimization problems, Optimal length cutting plane refutations of integer programs, Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces, Cutting planes cannot approximate some integer programs, Benchmarking a model checker for algorithmic improvements and tuning for performance, Unnamed Item, Lifting lower bounds for tree-like proofs, Resolution proof transformation for compression and interpolation, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, Interpolation and amalgamation for arrays with MaxDiff, Farkas-based tree interpolation, Copy complexity of Horn formulas with respect to unit read-once resolution, Propositional proof systems based on maximum satisfiability, On Interpolation in Decision Procedures, Parameterized Bounded-Depth Frege Is Not Optimal, Resolution over linear equations and multilinear proofs, On semantic cutting planes with very small coefficients, How to deal with unbelievable assertions, Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution, On the complexity of cutting-plane proofs using split cuts, Exploiting partial variable assignment in interpolation-based model checking, On the computational content of intuitionistic propositional proofs, The complexity of the Hajós calculus for planar graphs, Several notes on the power of Gomory-Chvátal cuts, Mean-payoff games and propositional proofs, Challenges in Constraint-Based Analysis of Hybrid Systems, Unnamed Item, Understanding cutting planes for QBFs, The Complexity of Propositional Proofs, Unnamed Item, Proof complexity of substructural logics, Approximation Refinement for Interpolation-Based Model Checking, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints, Ground Interpolation for the Theory of Equality, Efficient Interpolant Generation in Satisfiability Modulo Theories, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Efficient generation of small interpolants in CNF, Proof Complexity of Non-classical Logics, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, Propositional proof complexity, Unnamed Item, NIL: learning nonlinear interpolants, Complexity of branch-and-bound and cutting planes in mixed-integer optimization. II, Resolution for Max-SAT, Abstract Counterexamples for Non-disjunctive Abstractions, Some applications of propositional logic to cellular automata, \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver, Unnamed Item, An exponential lower bound for the size of monotone real circuits, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, No feasible monotone interpolation for simple combinatorial reasoning, High Degree Sum of Squares Proofs, Bienstock--Zuckerberg Hierarchy, and Chvátal--Gomory Cuts, An interpolating theorem prover, On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations, How QBF expansion makes strategy extraction hard, Space bounds for resolution, Lower bounds for the weak pigeonhole principle and random formulas beyond resolution, Interpolant Learning and Reuse in SAT-Based Model Checking, Reflections on Proof Complexity and Counting Principles

Cites Work