AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis
Abstract
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.
Cite
Text
Liang et al. "AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis." International Joint Conference on Artificial Intelligence, 2022. doi:10.24963/IJCAI.2022/259Markdown
[Liang et al. "AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis." International Joint Conference on Artificial Intelligence, 2022.](https://mlanthology.org/ijcai/2022/liang2022ijcai-allsatcc/) doi:10.24963/IJCAI.2022/259BibTeX
@inproceedings{liang2022ijcai-allsatcc,
title = {{AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis}},
author = {Liang, Jiaxin and Ma, Feifei and Zhou, Junping and Yin, Minghao},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2022},
pages = {1866-1872},
doi = {10.24963/IJCAI.2022/259},
url = {https://mlanthology.org/ijcai/2022/liang2022ijcai-allsatcc/}
}