# Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning

@article{Buss2008ResolutionTW, title={Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning}, author={Samuel R. Buss and Jan Hoffmann and Jan Johannsen}, journal={ArXiv}, year={2008}, volume={abs/0811.1075} }

Resolution refinements called w-resolution trees with lemmas (WRTL) and with
input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both
WRTL and WRTI when there is no regularity condition. For regular proofs, an
exponential separation between regular dag-like resolution and both regular
WRTL and regular WRTI is given.
It is proved that DLL proof search algorithms that use clause learning based
on unit propagation can be polynomially simulated by regular WRTI. More
generally… Expand

#### 56 Citations

Improved Separations of Regular Resolution from Clause Learning Proof Systems

- Mathematics, Computer Science
- J. Artif. Intell. Res.
- 2014

It is proved that the guarded, xor-ified pebbling tautology clauses, as well as the guarded graph tautOLOGY clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses, and it is extended to prove that a CDCL search without restarts can refute these clauses inPolynomial time. Expand

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning

- Mathematics, Computer Science
- SAT
- 2012

It is established that the sets of unsatisfiable clauses obtained from the guarded graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. Expand

Resolution and Clause Learning for Multi-Valued CNF Formulas

- Computer Science
- PRUV
- 2014

It is shown that Signed (or Multi-Valued) CNF formulas, and Regular Formulas, are possible reduction targets for a number of multi-valued logics and thus a possible basis for efficient reasoning systems for these logics. Expand

Width-Restricted Clause Learning and k-DNF Resolution

- 2021

The hierarchies of proof systems RTL(k) of Resolution trees with lemmas of width k and Res∗(k) of tree-like k-DNF Resolution lie between tree-like and dag-like Resolution in strength. We show that… Expand

Non-Restarting SAT Solvers with Simple Preprocessing Can Efficiently Simulate Resolution

- Computer Science
- AAAI
- 2014

This work studies non-restarting CDCL solvers that learn only one asserting clause per conflict and shows that, with simple preprocessing that depends only on the number of variables of the input formula, such solvers can polynomially simulate resolution. Expand

Exponential Separations in a Hierarchy of Clause Learning Proof Systems

- Computer Science, Mathematics
- SAT
- 2013

A resolution-based propositional proof system that is related to the DPLL algorithm with clause learning and its fragments are related to clause learning algorithms where the width of learned clauses is bounded by k. Expand

An Exponential Lower Bound for Width-Restricted Clause Learning

- Mathematics, Computer Science
- SAT
- 2009

It is shown by proving lower bounds on the proof length in a certain resolution proof system related to clause learning that the lower bound is of the same order of magnitude as a known lower bound for backtracking algorithms without any clause learning. Expand

Davis and Putnam Meet Henkin: Solving DQBF with Resolution

- Computer Science
- SAT
- 2021

This work presents a new decision procedure for DQBF in the style of Davis-Putnam resolution based on the merge resolution proof system, which directly constructs partial strategy functions for derived clauses and proves that the problem of evaluating DQ BF in H-Form is NEXP-complete. Expand

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

- Computer Science, Mathematics
- Electron. Colloquium Comput. Complex.
- 2020

A strengthening of the decision heuristic used in classical QCDCL, which does not necessarily decide variables in order of the prefix, but still allows to learn asserting clauses, and it is shown that with this decision policy, Q CDCL can be exponentially faster on some formulas. Expand

Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width

- Mathematics, Computer Science
- IJCAI
- 2011

It is shown that lower bounds on the runtime of width-restricted clause learning follow from lower boundson the width of resolution proofs, which yields the firstLower bounds on width- restricted clause learning for formulas in 3-CNF. Expand

#### References

SHOWING 1-10 OF 45 REFERENCES

Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning

- Mathematics, Computer Science
- LPAR
- 2005

It is shown that a certain family of formulas, called NT**(n) has polynomial sized pool-resolution refutations, whereas the shortest regular refutations have an exponential lower bound. Expand

Clause Learning Can Effectively P-Simulate General Propositional Resolution

- Computer Science
- AAAI
- 2008

This paper utilizes the idea of effective p-simulation, which is a new way of comparing clause learning with general resolution and other proof systems, and shows that pool proofs, a previously used characterization of clause learning, can effectively p-Simulate general resolution. Expand

Towards Understanding and Harnessing the Potential of Clause Learning

- Computer Science
- J. Artif. Intell. Res.
- 2004

The first precise characterization of clause learning as a proof system (CL) is presented, and it is shown that with a new learning scheme, CL can provide exponentially shorter proofs than many proper refinements of general resolution satisfying a natural property. Expand

On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems

- Mathematics, Computer Science
- SIAM J. Comput.
- 2000

An exponential lower bound for the size of tree-like cutting planes refutations of a certain family of conjunctive normal form (CNF) formulas with polynomial size resolution refutations is proved and an exponential separation between ordered and unrestricted resolution is proved. Expand

Regular Resolution Versus Unrestricted Resolution

- Mathematics, Computer Science
- SIAM J. Comput.
- 1993

An infinite family of unsatisfiable propositional formulas is constructed and the following shown: These formulas have polynomial size unrestricted resolution proofs, whereas all regular resolution proofs of these formulas are of superpolynomial length. Expand

Improvements to propositional satisfiability search algorithms

- Mathematics
- 1995

In this dissertation, we examine complete search algorithms for SAT, the satisfiability problem for propositional formulas in conjunctive normal form. SAT is NP-complete, easy to think about, and one… Expand

The Unit Proof and the Input Proof in Theorem Proving

- Mathematics, Computer Science
- JACM
- 1970

It is proved in the paper that a set S of clauses containing its unit factors has a unit proof if and only if S has an input proof. Expand

Using CSP Look-Back Techniques to Solve Real-World SAT Instances

- Computer Science
- AAAI/IAAI
- 1997

The results show that incorporating CSP look-back techniques renders easy many problems which otherwise are beyond DP's reach, and recommend that such techniques be included as options in implementations of DP, just as they are in systematic algorithms for the more general constraint satisfaction problem. Expand

Efficient conflict driven learning in a Boolean satisfiability solver

- Mathematics, Computer Science
- IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281)
- 2001

This paper generalizes various conflict driven learning strategies in terms of different partitioning schemes of the implication graph to re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Expand

Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle

- Computer Science
- ISAAC
- 1999

In the proof of a lower bound, a relationship between tree-like resolution and backtracking is exploited, which has long been recognized in this field but not been used before to give explicit results. Expand