AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis

AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis

Jiaxin Liang, Feifei Ma, Junping Zhou, Minghao Yin

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 1866-1872. https://doi.org/10.24963/ijcai.2022/259

All Solution SAT (AllSAT) is a variant of Propositional Satisfiability, which aims to find all satisfying assignments for a given formula. AllSAT has significant applications in different domains, such as software testing, data mining, and network verification. In this paper, observing that the lack of component analysis may result in more work for algorithms with non-chronological backtracking, we propose a DPLL-based algorithm for solving AllSAT problem, named AllSATCC, which takes advantage of component analysis to reduce work repetition caused by non-chronological backtracking. The experimental results show that our algorithm outperforms the state-of-the-art algorithms on most instances.
Keywords:
Constraint Satisfaction and Optimization: Satisfiabilty
Constraint Satisfaction and Optimization: Solvers and Tools