Extending Modern SAT Solvers for Enumerating All Models
Artificial Intelligence
2013-05-08 v2
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.
Keywords
Cite
@article{arxiv.1305.0574,
title = {Extending Modern SAT Solvers for Enumerating All Models},
author = {Said Jabbour and Lakhdar Sais and Yakoub Salhi},
journal= {arXiv preprint arXiv:1305.0574},
year = {2013}
}
Comments
This paper is withdrawn by the authors due to a missing reference. The authors work further on this issue and conduct exhaustive experimental comparison with other related works