ML Anthology

Accelerating SAT Solving by Common Subclause Elimination

Yaowei Yan, Chris E. Gutierrez, Jeriah Jn-Charles, Forrest Sheng Bao, Yuanlin Zhang
AAAI 2015 pp. 4224-4225
doi:10.1609/AAAI.V29I1.9732 /aaai/2015/yan2015aaai-accelerating/

Abstract

Boolean SATisfiability (SAT) is an important problem in AI. SAT solvers have been effectively used in important industrial applications including automated planning and verification. In this paper, we present novel algorithms for fast SAT solving by employing two common subclause elimination (CSE) approaches. Our motivation is that modern SAT solving techniques can be more efficient on CSE-processed instances. Empirical study shows that CSE can significantly speed up SAT solving.

PDF AAAI Semantic Scholar

Cite

Text

Yan et al. "Accelerating SAT Solving by Common Subclause Elimination." AAAI Conference on Artificial Intelligence, 2015. doi:10.1609/AAAI.V29I1.9732

Markdown

[Yan et al. "Accelerating SAT Solving by Common Subclause Elimination." AAAI Conference on Artificial Intelligence, 2015.](https://mlanthology.org/aaai/2015/yan2015aaai-accelerating/) doi:10.1609/AAAI.V29I1.9732

BibTeX

@inproceedings{yan2015aaai-accelerating,
  title     = {{Accelerating SAT Solving by Common Subclause Elimination}},
  author    = {Yan, Yaowei and Gutierrez, Chris E. and Jn-Charles, Jeriah and Bao, Forrest Sheng and Zhang, Yuanlin},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2015},
  pages     = {4224-4225},
  doi       = {10.1609/AAAI.V29I1.9732},
  url       = {https://mlanthology.org/aaai/2015/yan2015aaai-accelerating/}
}