Hard examples for resolution
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1361471
- scientific article; zbMATH DE number 1929954
- Theory and Applications of Models of Computation
- The intractability of resolution
- Hard examples for the bounded depth Frege proof system
- Resolution proofs of matching principles
- Width versus size in resolution proofs
- Width and size of regular resolution proofs
- scientific article; zbMATH DE number 1955763
- Space bounds for resolution
Cited in
(only showing first 100 items - show all)- A combinatorial characterization of treelike resolution space
- On threshold BDDs and the optimal variable ordering problem
- Resolution for Max-SAT
- Resolution vs. cutting plane solution of inference problems: Some computational experience
- Seventy-five problems for testing automatic theorem provers
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Unrestricted resolution versus N-resolution
- Tseitin's formulas revisited
- Complexity of resolution proofs and function introduction
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- An exponential lower bound for the size of monotone real circuits
- A lower bound for tree resolution
- The complexity of the pigeonhole principle
- 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.
- Simplified lower bounds for propositional proofs
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
- Resolution lower bounds for the weak functional 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
- Binary decision diagrams for first-order predicate logic.
- On hard instances
- Proving unsatisfiability of CNFs locally
- Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms
- Approximate counting in SMT and value estimation for probabilistic programs
- On subclasses of minimal unsatisfiable formulas
- Space bounds for resolution
- Resolution proofs of matching principles
- Resolution lower bounds for perfect matching principles
- On the complexity of resolution with bounded conjunctions
- A new algorithm for the propositional satisfiability problem
- Cutting planes, connectivity, and threshold logic
- An exponential separation between the parity principle and the pigeonhole principle
- Short resolution proofs for a sequence of tricky formulas
- The complexity of inverting explicit Goldreich's function by DPLL algorithms
- The symmetry rule in propositional logic
- Complexity analysis of propositional resolution with autarky pruning
- Recognition of tractable satisfiability problems through balanced polynomial representations
- Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
- Reversible pebble games and the relation between tree-like and general resolution space
- On Tseitin formulas, read-once branching programs and treewidth
- Non-clausal redundancy properties
- Bounded-depth Frege complexity of Tseitin formulas for all graphs
- Characterizing Tseitin-formulas with short regular resolution refutations
- Simulating strong practical proof systems with extended resolution
- Propositional proof systems based on maximum satisfiability
- Limitations of restricted branching in clause learning
- Some hard examples for the resolution method
- Resolution over linear equations modulo two
- Width versus size in resolution proofs
- Strong ETH and resolution via games and the multiplicity of strategies
- A taxonomy of exact methods for partial Max-SAT
- Semidefinite resolution and exactness of semidefinite relaxations for satisfiability
- Partition-based logical reasoning for first-order and propositional theories
- A combinatorial characterization of resolution width
- Several notes on the power of Gomory-Chvátal cuts
- Hard satisfiable instances for DPLL-type algorithms
- Typical case complexity of satisfiability algorithms and the threshold phenomenon
- Tractable approximate deduction for OWL
- 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
- A tutorial on time and space bounds in tree-like resolution
- Implicit resolution
- Space complexity in polynomial calculus
- Dynamic Symmetry Breaking by Simulating Zykov Contraction
- Polynomial size proofs of the propositional pigeonhole principle
- scientific article; zbMATH DE number 15495 (Why is no real title available?)
- Towards NP-P via proof complexity and search
- A finite state intersection approach to propositional satisfiability
- Construction of expanders and superconcentrators using Kolmogorov complexity
- Communication lower bounds via critical block sensitivity
- Cumulative space in black-white pebbling and resolution
- scientific article; zbMATH DE number 1361471 (Why is no real title available?)
- Exploiting parallelism: highly competitive semantic tree theorem prover
- DRAT and propagation redundancy proofs without new variables
- A Logical Autobiography
- Reflections on Proof Complexity and Counting Principles
- Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals
- A separator theorem for hypergraphs and a CSP-SAT algorithm
- Adventures in monotone complexity and TFNP
- Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
- scientific article; zbMATH DE number 7561756 (Why is no real title available?)
- Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs
- scientific article; zbMATH DE number 7250156 (Why is no real title available?)
- An Introduction to Lower Bounds on Resolution Proof Systems
- Monotone circuit lower bounds from resolution
- ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
- Variable and clause ordering in an FSA approach to propositional satisfiability
- The search efficiency of theorem proving strategies
- Supercritical space-width trade-offs for resolution
- From small space to small width in resolution
- Narrow proofs may be maximally long
- A Global Filtration for Satisfying Goals in Mutual Exclusion Networks
- On the resolution complexity of graph non-isomorphism
- The probabilistic analysis of a greedy satisfiability algorithm
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
This page was built for publication: Hard examples for resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3780485)
