TY - JOUR
T1 - Accelerating Boolean Satisfiability (SAT) solving by common subclause elimination
AU - Bao, Forrest Sheng
AU - Gutierrez, Chris
AU - Jn Charles-Blount, Jeriah
AU - Yan, Yaowei
AU - Zhang, Yuanlin
N1 - Publisher Copyright:
© 2017, Springer Science+Business Media Dordrecht.
PY - 2018/3/1
Y1 - 2018/3/1
N2 - Boolean Satisfiability (SAT) is an important problem in many domains. Modern SAT solvers have been widely used in important industrial applications including automated planning and verification. To solve more problems in real applications, new techniques are needed to speed up SAT solving. Inspired by the success of common subexpression elimination in programming languages and other related areas, we study the impact of common subclause elimination (CSE) on SAT solving. Intensive experiments on many SAT solvers and benchmarks with 48-h timeout show that CSE can consistently improve SAT solving. Up to 5% more SAT13 instances can be solved after CSE. LZW-based CSE shows the best overall performance, particularly in the category of application benchmarks. A potential use of this result is that one may consider the heuristic of applying CSE to boost SAT solver performance on real life applications. Because of many possible ways to improve the benefit of CSE, we hope future research can unleash the full potential of CSE in SAT solving.
AB - Boolean Satisfiability (SAT) is an important problem in many domains. Modern SAT solvers have been widely used in important industrial applications including automated planning and verification. To solve more problems in real applications, new techniques are needed to speed up SAT solving. Inspired by the success of common subexpression elimination in programming languages and other related areas, we study the impact of common subclause elimination (CSE) on SAT solving. Intensive experiments on many SAT solvers and benchmarks with 48-h timeout show that CSE can consistently improve SAT solving. Up to 5% more SAT13 instances can be solved after CSE. LZW-based CSE shows the best overall performance, particularly in the category of application benchmarks. A potential use of this result is that one may consider the heuristic of applying CSE to boost SAT solver performance on real life applications. Because of many possible ways to improve the benefit of CSE, we hope future research can unleash the full potential of CSE in SAT solving.
KW - Application benchmarks
KW - Boolean Satisfiability
KW - Common subclause elimination
UR - http://www.scopus.com/inward/record.url?scp=85009192357&partnerID=8YFLogxK
U2 - 10.1007/s10462-016-9530-6
DO - 10.1007/s10462-016-9530-6
M3 - Article
AN - SCOPUS:85009192357
SN - 0269-2821
VL - 49
SP - 439
EP - 453
JO - Artificial Intelligence Review
JF - Artificial Intelligence Review
IS - 3
ER -