A Study of Gaussian Elimination on Boolean Satisfiability and Craig Interpolation
Date Issued
2012
Date
2012
Author(s)
Han, Cheng-Shen
Abstract
The Boolean satisfiability problem (SAT) is one of the central problems in computer science of both theoretical and practical interests. SAT is the first discovered NP-complete problem, and many real-world computation problems, such as hardware and software verification, electronic design automation (EDA), artificial intelligence (AI), circuit design, automatic theorem proving, etc., can be naturally encoded as SAT instances and solved efficiently. Although impressive advancements of SAT solving have been achieved, recent research reveals modern solvers'' inability to handle formulae in the abundance of parity xor constraints. Although xor-handling in SAT solving has attracted much attention, challenges remain to completely deduce xor-inferred implications and conflicts, to effectively reduce expensive overhead, and to directly generate compact interpolants. This thesis presents a new SAT solver, SimpSat, which integrates SAT solving tightly with Gaussian elimination in the style of Dantzig''s simplex method. It yields a powerful tool overcoming these challenges. Experiments show promising performance improvements and efficient derivation of compact interpolants, which are otherwise unobtainable.
Subjects
Boolean satisfiability
Craig interpolation
Gaussian elimination
xor-handling
xor constraints
SDGs
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-101-R99943082-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):81459898079b765286103dedbd1d7013