What we can learn from conflicts in propositional satisfiability

What we can learn from conflicts in propositional satisfiability

0.00 Avg rating0 Votes
Article ID: iaor20162274
Volume: 240
Issue: 1
Start Page Number: 13
End Page Number: 37
Publication Date: May 2016
Journal: Annals of Operations Research
Authors: , ,
Keywords: learning, artificial intelligence
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.

Reviews

Required fields are marked *. Your email address will not be published.