Issue No. 03 - March (2012 vol. 61)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2010.270
Liangze Yin , Sch. of Software, Tsinghua Univ., Beijing, China
Fei He , Sch. of Software, Tsinghua Univ., Beijing, China
William N. N. Hung , Verification Group, Synopsys Inc., Mountain View, CA, USA
Xiaoyu Song , Dept. of ECE, Portland State Univ., Portland, OR, USA
Ming Gu , Sch. of Software, Tsinghua Univ., Beijing, China
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.
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
W. N. Hung, Fei He, Liangze Yin, Xiaoyu Song and Ming Gu, "Maxterm Covering for Satisfiability," in IEEE Transactions on Computers, vol. 61, no. , pp. 420-426, 2012.