Source-linked AI summary
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
Albert Atserias, Johannes Klaus Fichte, Marc Thurley
TL;DR
The paper asks how practical DPLL-based SAT-solvers can be understood without relying on ideal nondeterministic choices. It analyzes a concrete randomized clause-learning algorithm and proves that it simulates bounded-width resolution with a polynomially bounded number of conflicts and restarts.
Problem
Existing proof-complexity analyses characterize SAT-solvers using resolution systems, but the paper seeks positive results without ideal nondeterministic choices.
Method
The paper analyzes a solver using unit propagation, clause learning, restarts, and random decisions, proving simulation through clause absorption rather than direct learning of the refutation.
Results
Width-k resolution is simulated with probability at least 1/2 using at most O(k^2 ln(kn)n^(2k+1)) conflicts and deterministic restarts.
Takeaways & Limitations
The result yields polynomial-time solving for 2-SAT and bounded-treewidth formulas and connects width-k resolution with repeated unit-clause propagation.
Takeaways & Limitations
The analysis crucially assumes that learned clauses are never removed, unlike practical solvers that periodically delete learned clauses.
Abstract
from arXiv · showhide
We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a concrete algorithm which we claim is faithful to what practical solvers do. In particular, before making any new decision or restart, the solver repeatedly applies the unit-resolution rule until saturation, and leaves no component to the mercy of non-determinism except for some internal randomness. We prove the perhaps surprising fact that, although the solver is not explicitly designed for it, with high probability it ends up behaving as width-k resolution after no more than O(n^2k+2) conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as O(n^2k+2) restarts of the unit-resolution rule with learning.
1. Introduction
The paper analyzes practical SAT-solvers through proof complexity while avoiding most nondeterministic choices. It shows that randomized clause-learning solvers can simulate bounded-width resolution and yields consequences for several formula classes.
- Contribution: The paper studies a concrete SAT-solver family that uses clause learning, unit propagation, restarts, and only mild randomness.Its analysis aims to avoid nondeterminism in the solver's components while retaining practical design features.
- Main result: With probability at least 1/2, totally random decisions require at most O(k^2 ln(kn)n^(2k+1)) conflicts and deterministic restarts for width-k refutations.The bound is stated as an exact expression valid for all n and k, rather than only asymptotically.
- Consequences: The result connects repeated unit-clause propagation with width-k resolution and implies polynomial-time solving for 2-SAT and bounded-treewidth formulas.It also gives quasipolynomial or subexponential consequences for formulas with suitable polynomial-size resolution proofs.
- Technique: The analysis proves absorption of every width-k clause rather than showing that the refutation itself is learned.The produced proof may have much larger width, but absorption makes the algorithm behave as if the clauses had been learned.
- Related work: The work extends proof-complexity analyses of clause-learning solvers by addressing standard algorithms without ideal decision strategies or multiple assignments.It introduces clause-absorption to analyze these algorithms directly.
2. Clause Learning Algorithms
This section introduces the algorithmic framework and situates the paper's definitions relative to prior work.
- Algorithm framework: The section begins by defining the algorithm and discussing choices for its components.These components include the learning scheme, restart policy, and decision strategy.
- Organization: The framework is presented alongside preliminary definitions needed for the subsequent algorithmic analysis.The supplied section-opening text points forward to these definitions.
- Related concepts: A footnote records that a weaker version of 1-empowerment was originally introduced by Pipatsrisawat and Darwiche in 2008.The note distinguishes the cited original version from later formulations.
2.1 Preliminaries
The preliminaries define clauses, CNF formulas, restrictions, and resolution refutations, establishing the notation used to analyze solver behavior.
- Basic notation: A clause is a set of literals, and a CNF formula is a set of clauses over a fixed variable set.The width of a clause is its number of literals.
- Resolution: Resolution combines clauses containing complementary literals to form a resolvent after removing the resolved variable and its complement.The resolvent remains well-defined even when a clause contains both a literal and its negation.
- Resolution: A resolution refutation is a clause sequence ending in the empty clause, with each clause either an input clause or a resolvent of earlier clauses.Its length is the number of clauses in the sequence.
- Restrictions: Restricting a clause by a partial assignment removes satisfied clauses and falsified literals according to the assignment.A partial assignment satisfies a clause when at least one literal is satisfied and falsifies it when the restricted clause is empty.
2.2 Definition of the Algorithm
The algorithm maintains a state and clause set, alternating among propagation, decisions, conflict learning, and restarts until it derives SAT or UNSAT.
- State representation: The solver state records assignments and decision marks, while decision levels count the number of decisions preceding each assignment.Assignments not marked as decisions are implied assignments.
- Modes of operation: In DEFAULT mode, the solver checks satisfaction, detects conflicts, prioritizes unit clauses, and otherwise invokes the decision strategy.This ordering ensures that unit propagation is applied before new decisions.
- Modes of operation: After a conflict, the solver learns a clause, may restart, or backtracks until the learned clause becomes unit before continuing propagation.Learning the empty clause terminates with UNSAT.
- Modes of operation: The UNIT mode assigns the value required by a unit clause, whereas DECISION mode adds an assignment selected by the decision strategy.Both modes return control to DEFAULT.
- Learning scheme: Learned clauses are logical consequences, falsified by the current state, and contain at most one variable at the maximum decision level.These conditions support correctness, termination, and the availability of asserting clauses.
- Relation to DPLL: Unlike DPLL, the algorithm combines clause learning, non-chronological backtracking, restart policies, and decision strategies.DPLL instead performs no learning or restarts and backtracks chronologically.
- Rounds: A round is a sequence of states extending by one unit or decision assignment until a conflict or an inconclusive stopping condition.A complete round ends when all variables are assigned or a falsified clause is found; satisfying assignments are inconclusive.
2.3 Restart Policy, Learning Scheme, and Decision Strategy
The algorithm’s analysis depends on frequent restarts, occasional totally random decisions, and asserting clause learning. It also assumes learned clauses are retained and may require clauses of unrestricted width.
- Restart policy: Frequent restarts are sufficient for the analysis, ranging from restarting after every conflict to allowing any bounded number of conflicts between restarts.The analysis is stated to be insensitive to this choice within the bounded-conflict condition.
- Decision strategy: A decision strategy must allow totally random rounds often enough, while boundedly many heuristic decisions may intervene at a multiplicative cost.A totally random decision chooses an unset variable and truth value independently and uniformly.
- Learning scheme: The learning scheme constructs conflict clauses by reverse resolution through implied assignments and adds an asserting clause after each conflict.Decision learning adds A1, while 1UIP learning adds the latest Ai that is asserting.
- Learning scheme: The analysis assumes an asserting learning scheme, whose learned clauses have at most one variable at the maximum decision level, except for the empty clause.This assumption includes the Decision and 1UIP schemes described in the passage.
- Clause bookkeeping: The analysis crucially assumes learned clauses are never deleted, whereas practical solvers periodically remove clauses to save memory and reduce overhead.The authors note that proof-complexity results suggest a similar retention assumption may be necessary.
- Clause width: The analysis does not appear to support restricting learning to short clauses only, and prior results show that such restriction can be weaker than learning arbitrarily long clauses.The cited examples do not establish that long clauses are required for small-width simulations, but the authors consider this possible.
3. Analysis of the Algorithm
The running-time analysis introduces absorption and beneficial rounds as technical concepts whose properties are needed to analyze the algorithm.
- Technical framework: The analysis studies running time through the concepts of absorption and beneficial rounds.The authors introduce these concepts before analyzing the algorithm’s running time.
3.1 Runs of the Algorithm
The runs analysis formalizes how rounds proceed under propagation and decisions, and proves robustness of inconclusive rounds under changes in assignment order and clause sets.
- Round relations: Rounds are compared using subsumption, agreement on a clause, and branching in a clause.Agreement depends on assignments to variables in the clause, while branching requires all decision variables to occur there.
- Robustness lemmas: Inconclusive rounds are robust: an inconclusive round over a larger clause set subsumes every compatible round over a subset that branches in and agrees on the relevant clause.This is the content of Lemma 1.
- Robustness lemmas: For any inconclusive round over a larger clause set, there exists a compatible inconclusive round over the smaller set that branches in the chosen clause and is subsumed by it.This is the existence statement of Lemma 2.
- Round construction: A round is constructed by repeatedly applying unit propagation, then selecting the minimum-index unset variable for a decision, and stopping on conflict, completion, or exhaustion of applicable steps.The construction starts from the empty state and tracks variables left unassigned.
- Round construction: The constructed round is valid, is inconclusive when the larger round is inconclusive, subsumes the relevant assignments, agrees on the chosen clause, and branches in that clause.These properties follow from the construction and the stated subsumption relation.
3.2 Absorption
Absorption captures clauses enforced by unit propagation on every inconclusive round. It is monotone, implies logical consequence, and is dual to 1-empowerment for clauses that follow from the current clause set.
- Definition and intuition: A clause is absorbed at a literal when every inconclusive round falsifying its other literals assigns that literal true; it is absorbed when this holds for every literal.Absorption formalizes clauses learned implicitly through propagation.
- Examples: A clause absent from the clause set can still be absorbed: in the example, propagation forces c when a is false and a when c is false.The example uses the clause a ∨c and shows absorption without explicit membership.
- Logical consequences: If a clause is absorbed, it is a logical consequence of the clause set.This establishes absorption as a sound implicit-learning notion, though the converse does not hold.
- Limits of absorption: Logical consequence does not imply absorption; the example gives a resolvent that follows from D but is not absorbed by D.The authors also identify a condition on a non-absorbed resolvent of two absorbed clauses: its problematic literal appears in both parents.
- Monotonicity: Absorption is monotone: clauses in D are absorbed by D, supersets of absorbed clauses are absorbed, and enlarging D preserves absorption.These are the three properties stated in Lemma 5.
- Absorption and empowerment: The duality is reflected operationally: a non-absorbed entailed clause has an inconclusive round that falsifies all other literals without assigning the remaining one.This witness is exactly the configuration used to characterize 1-empowerment.
- Absorption and empowerment: For a clause entailed by D, failure to absorb it at a literal is equivalent to 1-empowerment through that literal.The definition of 1-empowerment requires entailment, non-contradictory propagation, and failure to assign the target literal.
3.3 Beneficial Rounds
Beneficial rounds expose when an absorbed pair of clauses yields a resolvent that is not yet absorbed, and provide a witness that can drive its eventual absorption.
- Structural property: A non-absorbed resolvent C of absorbed resolvable clauses A and B has every unabsorbed literal appearing in both A and B.This structural property links clause absorption to merge resolution and explains how resolution can be simulated.
- Role in the simulation: Beneficial rounds therefore provide the operational witness that lets the algorithm progress from absorbed premises toward absorption of their resolvent.The proof identifies a literal at which the round can be constructed.
- Definition: A beneficial round for A at literal x_a falsifies A without x_a, branches within that reduced clause, leaves x unassigned, and becomes conclusive when x is assigned its satisfying value.Such a round witnesses that A is almost absorbed at x_a.
- Existence: If C is a non-empty, non-absorbed resolvent of absorbed clauses A and B, some round started from the current clause set is beneficial for C.The construction extends an inconclusive round by the opposite assignment, forcing a conclusive round because A and B are absorbed.
3.4 Main Technical Lemma
The main technical lemma bounds the probability that repeated random rounds fail both to produce a beneficial round and to absorb a resolvent.
- Setup: A beneficial round is the prerequisite analyzed before bounding the time needed for a resolvent to become absorbed.The analysis first estimates the waiting time for this prerequisite.
- Failure bound: For t consecutive rounds, the probability that no round is beneficial and no intermediate clause set absorbs C is at most e^(-t/(4nk)).Here n is the number of variables and k is the width of the non-empty resolvent C.
- Proof strategy: The proof conditions on the preceding rounds and bounds the probability of each failure event before multiplying the resulting conditional bounds.The argument uses the existence of a beneficial round and a lower bound on the random decision sequence that realizes it.
- Random strategy: The required decision sequence falsifies the other k−1 literals of C and then chooses the target variable with the opposite value.Its probability is bounded below by 1/(4n^k).
- Round construction: Once the relevant decisions are made, subsequent unit propagation preserves the assignments needed for the round to become beneficial.The argument uses subsumption and the fact that the resulting decision completes the conclusive round.
3.5 Bounds
The bounds show that repeated randomized rounds simulate bounded-width resolution with high probability, first directly for Decision learning and then for arbitrary asserting schemes.
- Decision learning: For Decision learning, a beneficial round immediately causes absorption of the resolvent because the learned clause is a subset of it.This yields a per-resolvent failure probability of at most e^(-t/(4nk)) after t restarts.
- Decision learning: With probability at least 1/2, Decision learning learns the empty clause within 4m ln(4m)n^k conflicts and restarts for a width-k refutation of length m.The proof accumulates absorption guarantees along resolution proofs leading to the final unit clauses.
- General asserting schemes: For arbitrary asserting learning schemes, adding learned clauses cannot create new beneficial literals and cannot increase the associated unassigned-variable measure.These monotonicity properties support the more involved absorption analysis.
- General asserting schemes: A beneficial round strictly decreases the relevant progress measures under an arbitrary asserting scheme, even though its learned clause need not be a subset of the resolvent.This is the key detour beyond the Decision-learning argument.
- General asserting schemes: For arbitrary asserting learning schemes, the probability that a width-k resolvent remains unabsorbed after kn·t restarts is at most kn·e^(-t/(4nk)).The additional kn factor reflects the more complex route from beneficial rounds to absorption.
- General asserting schemes: With probability at least 1/2, the general asserting-scheme algorithm learns the empty clause within 4km ln(4knm)n^(k+1) conflicts and restarts.The result applies to formulas with a width-k resolution refutation of length m.
4. Consequences
The consequences bound the relevant refutation size, establish a probabilistic learning guarantee, and extend the algorithm to bounded-treewidth CNF formulas. The resulting procedure decides satisfiability within an explicit parameterized running time and supports assignment recovery by self-reducibility.
- A width-k resolution refutation can be assumed to have length at most 4nk.
- With probability at least 1/2, the algorithm learns the empty clause after at most 16k(k + 1) ln(16kn)n2k+1.
- CNF formulas of treewidth at most k can be decided in time O(k2 log(kn)n2k+3).
- Using self-reducibility, all assignment iterations are correct with probability at least 1/2, with total running time O(k2(log(kn))2n2k+4).