The Community for Technology Leaders
Green Image
Issue No. 03 - March (2012 vol. 61)
ISSN: 0018-9340
pp: 420-426
William N. N. Hung , Verification Group, Synopsys Inc., Mountain View, CA, USA
Fei He , Sch. of Software, Tsinghua Univ., Beijing, China
Liangze Yin , Sch. of Software, Tsinghua Univ., Beijing, China
Xiaoyu Song , Dept. of ECE, Portland State Univ., Portland, OR, USA
Ming Gu , Sch. of Software, Tsinghua Univ., Beijing, China
ABSTRACT
This paper presents a novel efficient satisfiability (SAT) algorithm based on maxterm covering. The satisfiability of a clause set is determined in terms of the number of relative maxterms of the empty clause with respect to the clause set. If the number of relative maxterms is zero, it is unsatisfiable, otherwise satisfiable. A set of synergic heuristic strategies are presented and elaborated. We conduct a number of experiments on 3-SAT and k-SAT problems at the phase transition region, which have been cited as the hardest group of SAT problems. Our experimental results on public benchmarks attest to the fact that, by incorporating our proposed heuristic strategies, our enhanced algorithm runs several orders of magnitude faster than the extension rule algorithm, and it also runs faster than zChaff and MiniSAT for most of k-SAT (k≥3) instances.
INDEX TERMS
formal verification, Boolean functions, computability, MiniSAT, efficient satisfiability algorithm, maxterm covering, clause set, synergic heuristic strategy, k-SAT problem, phase transition region, extension rule algorithm, zChaff, Optimization, Complexity theory, Arrays, Acceleration, Runtime, Optical wavelength conversion, heuristics., Verification, satisfiability, maxterm covering
CITATION
William N. N. Hung, Fei He, Liangze Yin, Xiaoyu Song, Ming Gu, "Maxterm Covering for Satisfiability", IEEE Transactions on Computers, vol. 61, no. , pp. 420-426, March 2012, doi:10.1109/TC.2010.270
189 ms
(Ver 3.3 (11022016))