Application of Graph Automorphism on Improving SAT Solver Performance
Date Issued
2011
Date
2011
Author(s)
Lin, Chun-Xun
Abstract
NP-complete problems are often seen in different areas, but there is no proof showing NP equals P up to present and thus no polynomial time algorithms exist to give an optimal solution for NP-complete problems. Among all NP-complete problems, Boolean satisfiability is the first proven NP-complete problem and received widely study and found applications in artificial intelligence, computational theory, formal verification and electronic design automation(EDA) related areas.For Boolean satisfiability problem, SAT solver is the mainstream method,
although many problems can be solved by SAT solver in reasonable time, but in terms of complexity, SAT solver still is of exponential time, so there are still lots of intractable problems. In this dissertation,a flow is implemented by transforming the Boolean satisfiability problem into a graph, and then using the graph automorphism algorithm to search for symmetries between variables. The symmetries found can prune the solution space, and finally a Boolean representation of symmetries is provided to SAT solver to accelerate its speed. The experimental
results show that searching for symmetries requires additional time though,but the symmetries reduce the execution time of SAT solver substantially and
therefore improve the whole performance.
Subjects
Boolean satisfiability problem
graph automorphism
SAT solver
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-100-R98943096-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):b4195f53740bebab13320a78efc1b9d5