Hard examples for resolution

DOI10.1145/7531.8928zbMath0639.68093OpenAlexW2098022011MaRDI QIDQ3780485

Alasdair Urquhart

Publication date: 1987

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/7531.8928

zbMATH Keywords

complexity of proofsexpander graphsresolution proofsmechanical theorem provingrefutationshard examplespigeonhole clauses

Mathematics Subject Classification ID

Related Items (only showing first 100 items - show all)

Characterizing Tseitin-Formulas with Short Regular Resolution Refutations ⋮ Depth lower bounds in Stabbing Planes for combinatorial principles ⋮ Are hitting formulas hard for resolution? ⋮ Constructions of strongly regular Cayley graphs derived from weakly regular bent functions ⋮ Linear gaps between degrees for the polynomial calculus modulo distinct primes ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution ⋮ The probabilistic analysis of a greedy satisfiability algorithm ⋮ MaxSAT Resolution and Subcube Sums ⋮ From Small Space to Small Width in Resolution ⋮ Narrow Proofs May Be Maximally Long ⋮ Tractable approximate deduction for OWL ⋮ Resolution lower bounds for perfect matching principles ⋮ A lower bound for tree resolution ⋮ On the complexity of resolution with bounded conjunctions ⋮ The complexity of the pigeonhole principle ⋮ Cumulative Space in Black-White Pebbling and Resolution ⋮ Smaller superconcentrators of density 28 ⋮ A new algorithm for the propositional satisfiability problem ⋮ Width versus size in resolution proofs ⋮ The relative complexity of resolution and cut-free Gentzen systems ⋮ Davis-Putnam resolution versus unrestricted resolution ⋮ An average case analysis of a resolution principle algorithm in mechanical theorem proving. ⋮ A Global Filtration for Satisfying Goals in Mutual Exclusion Networks ⋮ Resolution vs. cutting plane solution of inference problems: Some computational experience ⋮ Seventy-five problems for testing automatic theorem provers ⋮ Communication Lower Bounds via Critical Block Sensitivity ⋮ Exploiting parallelism: highly competitive semantic tree theorem prover ⋮ Cutting planes, connectivity, and threshold logic ⋮ Optimizing propositional calculus formulas with regard to questions of deducibility ⋮ Simplified lower bounds for propositional proofs ⋮ Proof complexity in algebraic systems and bounded depth Frege systems with modular counting ⋮ Strong ETH and resolution via games and the multiplicity of strategies ⋮ An exponential separation between the parity principle and the pigeonhole principle ⋮ Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms ⋮ Space Complexity in Polynomial Calculus ⋮ Unnamed Item ⋮ Approximate counting in SMT and value estimation for probabilistic programs ⋮ Towards NP-P via proof complexity and search ⋮ Resolution lower bounds for the weak functional pigeonhole principle. ⋮ Polynomial size proofs of the propositional pigeonhole principle ⋮ Resolution and binary decision diagrams cannot simulate each other polynomially ⋮ On the structure of some classes of minimal unsatisfiable formulas ⋮ Equivalent literal propagation in the DLL procedure ⋮ The complexity of inverting explicit Goldreich's function by DPLL algorithms ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ A finite state intersection approach to propositional satisfiability ⋮ Simulating strong practical proof systems with extended resolution ⋮ A feasibly constructive lower bound for resolution proofs ⋮ Resolution proofs of generalized pigeonhole principles ⋮ The symmetry rule in propositional logic ⋮ Complexity analysis of propositional resolution with autarky pruning ⋮ Recognition of tractable satisfiability problems through balanced polynomial representations ⋮ Binary decision diagrams for first-order predicate logic. ⋮ Semidefinite resolution and exactness of semidefinite relaxations for satisfiability ⋮ An Introduction to Lower Bounds on Resolution Proof Systems ⋮ Unnamed Item ⋮ Formula dissection: A parallel algorithm for constraint satisfaction ⋮ Partition-based logical reasoning for first-order and propositional theories ⋮ ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES ⋮ Unrestricted resolution versus N-resolution ⋮ Meta-resolution: An algorithmic formalisation ⋮ Tractability of cut-free Gentzen type propositional calculus with permutation inference ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ Propositional proof systems based on maximum satisfiability ⋮ Tseitin's formulas revisited ⋮ Complexity of resolution proofs and function introduction ⋮ A combinatorial characterization of resolution width ⋮ Exponential lower bounds for the pigeonhole principle ⋮ Construction of expanders and superconcentrators using Kolmogorov complexity ⋮ Highly symmetric expanders ⋮ Limitations of restricted branching in clause learning ⋮ Several notes on the power of Gomory-Chvátal cuts ⋮ A simplified way of proving trade-off results for resolution ⋮ Unnamed Item ⋮ Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability ⋮ Reversible pebble games and the relation between tree-like and general resolution space ⋮ The search efficiency of theorem proving strategies ⋮ On tseitin formulas, read-once branching programs and treewidth ⋮ Supercritical Space-Width Trade-offs for Resolution ⋮ A combinatorial characterization of treelike resolution space ⋮ On threshold BDDs and the optimal variable ordering problem ⋮ Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space ⋮ Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle ⋮ Improved Static Symmetry Breaking for SAT ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Non-clausal redundancy properties ⋮ Unnamed Item ⋮ A Tutorial on Time and Space Bounds in Tree-Like Resolution ⋮ Dynamic Symmetry Breaking by Simulating Zykov Contraction ⋮ Adventures in monotone complexity and TFNP ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ Resolution for Max-SAT ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Unnamed Item ⋮ An exponential lower bound for the size of monotone real circuits ⋮ Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs. ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ On subclasses of minimal unsatisfiable formulas ⋮ Resolution over linear equations modulo two

This page was built for publication: Hard examples for resolution