What we can learn from conflicts in propositional satisfiability

Youssef Hamadi (), Saïd Jabbour () and Lakhdar Saïs ()
Additional contact information
Youssef Hamadi: Microsoft Research
Saïd Jabbour: CRIL-CNRS, Université Lille Nord de France - Artois
Lakhdar Saïs: CRIL-CNRS, Université Lille Nord de France - Artois

Annals of Operations Research, 2016, vol. 240, issue 1, No 3, 13-37

Abstract: Abstract Learning is a general concept, playing an important role in many Artificial intelligence domains. In this paper, we address the learning paradigm used to explain failures or conflicts encountered during search. This explanation, derived by conflict analysis, and generally expressed as a new constraint, is usually used to dynamically avoid future occurrences of similar situations. Before focusing on clause learning in Boolean satisfiability (SAT), we first overview some important works on this powerful reasoning tool in other domains such as constraint satisfaction and truth maintenance systems. Then, we present a comprehensive survey of the most important works having led to what is called today—conflict driven clause learning—which is one of the key components of modern SAT solvers. We also overview some of the original extensions or variants of clauses learning. In theory, current SAT solvers with clause learning are as powerful as general resolution proof systems. In practice, real-world SAT instances with millions of variables and clauses are now in the scope of this solving paradigm.

Keywords: Propositional satisfiability; Constraint solving; Reasoning; SAT (search for similar items in EconPapers)
Date: 2016
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s10479-015-2028-9 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:annopr:v:240:y:2016:i:1:d:10.1007_s10479-015-2028-9

Ordering information: This journal article can be ordered from
http://www.springer.com/journal/10479

DOI: 10.1007/s10479-015-2028-9

Access Statistics for this article

Annals of Operations Research is currently edited by Endre Boros

More articles in Annals of Operations Research from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().