Accelerating SAT Solving by Common Subclause Elimination

Authors

  • Yaowei Yan University of Akron
  • Chris Gutierrez Texas Tech University
  • Jeriah Jn-Charles Texas Tech University
  • Forrest Bao University of Akron
  • Yuanlin Zhang Texas Tech University

DOI:

https://doi.org/10.1609/aaai.v29i1.9732

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.

AAAI 2015 Proceedings Cover

Downloads

Published

2015-03-04

How to Cite

Yan, Y., Gutierrez, C., Jn-Charles, J., Bao, F., & Zhang, Y. (2015). Accelerating SAT Solving by Common Subclause Elimination. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1). https://doi.org/10.1609/aaai.v29i1.9732

Issue

Vol. 29 No. 1 (2015): Twenty-Ninth AAAI Conference on Artificial Intelligence

Section

Student Abstract Track