Extending Modern SAT Solvers for Enumerating All Models

2013/05/02 by Jabbour, Said, Sais, Lakhdar, Salhi, Yakoub
#Artificial Intelligence (cs.AI) #FOS: Computer and information sciences

paper · doi:10.48550/arxiv.1305.0574

Abstract

In this paper, we address the problem of enumerating all models of a Boolean formula in conjunctive normal form (CNF). We propose an extension of CDCL-based SAT solvers to deal with this fundamental problem. Then, we provide an experimental evaluation of our proposed SAT model enumeration algorithms on both satisfiable SAT instances taken from the last SAT challenge and on instances from the SAT-based encoding of sequence mining problems.

Related

• On Enumerating Short Projected Models
• On CNF Conversion for SAT and SMT Enumeration
• Mining to Compact CNF Propositional Formulae
• On SAT Models Enumeration in Itemset Mining
• Sub-exponential Upper Bound for #XSAT of some CNF Classes