Clause Learning Algorithm

Context:
- It can be a Constraint Learning Algorithm.
- It requires a Learning Scheme.
- …
Example(s):
- Default Clause.
- Conflict Clause.
- Unit Clause.
- Decision Clause.
Counter-Example(s)
- Conflict-Driven Clause Learning
See: Learned Clause, Propositional Satisfiability, Constraint Satisfaction Problem, Backtracking, Algorithm, Candidate Solution.

References

(Wikipedia, 2017) ⇒ https://en.wikipedia.org/wiki/Constraint_learning Retrieved:2017-5-28.
- In constraint satisfaction backtracking algorithms, constraint learning is a technique for improving efficiency. It works by recording new constraints whenever an inconsistency is found. This new constraint may reduce the search space, as future partial evaluations may be found inconsistent without further search. Clause learning is the name of this technique when applied to propositional satisfiability.

(Sammut & Webb, 2011) ⇒ Claude Sammut (editor), and Geoffrey I. Webb (editor). (2011). “Clause Learning.” In: (Sammut & Webb, 2011) p.179
- QUOTE: In speedup learning, clause learning is a deductive learning technique used for the purpose of intelligent backtracking in satisfiability solvers. The approach analyzes failures at backtracking points and derives clauses that must be satisfied by the solution. The clauses are added to the set of clauses from the original satisfiability problem and serve to prune new search nodes that violate them.

(Atserias et al., 2011) ⇒ Atserias, A., Fichte, J. K., & Thurley, M. (2011). “Clause-learning algorithms with many restarts and bounded-width resolution". Journal of Artificial Intelligence Research, 40, 353-373. [1]
- 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 [math]\displaystyle{ O(n^{2k+2}) }[/math] conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as [math]\displaystyle{ O(n^{2k+2}) }[/math] restarts of the unit-resolution rule with learning.

(Tichy & Glase) ⇒ Tichy, R., & Glase, T. (2006). Clause Learning in SAT. https://www.cs.princeton.edu/courses/archive/fall13/cos402/readings/SAT_learning_clauses.pdf
- Abstract: The development of clause learning has had a tremendous effect on the overall performance of SAT-Solvers. Clause learning has allowed SAT-Solvers to tackle industrial sized problems that formerly would have required impractical time scales. The development of techniques for efficient clause management and storage have also proved important in reducing some of the memory usage problems inherent in naive clause learning strategies. This paper attempts an introduction to some better known clause-learning strategies as a comparison among these strategies. A brief explanation of some of the techniques available to minimize memory usage when storing learned clauses in a database is also presented.