Clause Learning Algorithm

From GM-RKB
(Redirected from Clause Learning)
Jump to navigation Jump to search

A Clause Learning Algorithm is a deductive learning algorithm that ...



References

2017

2011a

2011B

  • (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.

2006

  • (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.