This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Maxterm Covering for Satisfiability
March 2012 (vol. 61 no. 3)
pp. 420-426
ASCII Text
x 
 
Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song, Ming Gu, "Maxterm Covering for Satisfiability," IEEE Transactions on Computers, vol. 61, no. 3, pp. 420-426, March, 2012.
 
 
BibTex
x
 
@article{ 10.1109/TC.2010.270,
author = { Liangze Yin and Fei He and William N. N. Hung and Xiaoyu Song and Ming Gu},
title = {Maxterm Covering for Satisfiability},
journal ={IEEE Transactions on Computers},
volume = {61},
number = {3},
issn = {0018-9340},
year = {2012},
pages = {420-426},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2010.270},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - Maxterm Covering for Satisfiability
IS - 3
SN - 0018-9340
SP420
EP426
EPD - 420-426
A1 - Liangze Yin,
A1 - Fei He,
A1 - William N. N. Hung,
A1 - Xiaoyu Song,
A1 - Ming Gu,
PY - 2012
KW - formal verification
KW - Boolean functions
KW - computability
KW - MiniSAT
KW - efficient satisfiability algorithm
KW - maxterm covering
KW - clause set
KW - synergic heuristic strategy
KW - k-SAT problem
KW - phase transition region
KW - extension rule algorithm
KW - zChaff
KW - Optimization
KW - Complexity theory
KW - Arrays
KW - Acceleration
KW - Runtime
KW - Optical wavelength conversion
KW - heuristics.
KW - Verification
KW - satisfiability
KW - maxterm covering
VL - 61
JA - IEEE Transactions on Computers
ER -
 
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.

[1] S.A. Cook, “The Complexity of Theorem-Proving Procedures,” Proc. Third ACM Symp. Theory of Computing, pp. 151-158, 1971.
[2] T. Larrabee, “Test Pattern Generation Using Boolean Satisfiability,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 11, no. 1, pp. 4-15, Jan. 1992.
[3] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proc. Design Automation Conf., pp. 317-320, 1999.
[4] W.N.N. Hung and N. Narasimhan, “Reference Model Based RTL Verification: An Integrated Approach,” Proc. IEEE Int'l High Level Design Validation and Test Workshop (HLDVT), pp. 9-13, Nov. 2004.
[5] W.N.N. Hung, X. Song, G. Yang, J. Yang, and M. Perkowski, “Optimal Synthesis of Multiple Output Boolean Functions Using a Set of Quantum Gates by Symbolic Reachability Analysis,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 9, pp. 1652-1663, Sept. 2006.
[6] W.N.N. Hung, C. Gao, X. Song, and D. Hammerstrom, “Defect Tolerant CMOL Cell Assignment via Satisfiability,” IEEE Sensors J., vol. 8, no. 6, pp. 823-830, June 2008.
[7] R.G. Wood and R.A. Rutenbar, “FPGA Routing and Routability Estimation via Boolean Satisfiability,” Proc. Int'l Symp. Field-Programmable Gate Arrays, pp. 119-125, 1997.
[8] X. Song, W.N.N. Hung, A. Mishchenko, M. Chrzanowska-Jeske, A. Kennings, and A. Coppola, “Board-Level Multiterminal Net Assignment for the Partial Cross-Bar Architecture,” IEEE Trans. Very Large Scale Integration Systems, vol. 11, no. 3, pp. 511-514, June 2003.
[9] W.N.N. Hung, X. Song, T. Kam, L. Cheng, and G. Yang, “Routability Checking for Three-Dimensional Architectures,” IEEE Trans. Very Large Scale Integration Systems, vol. 12, no. 12, pp. 1398-1401, Dec. 2004.
[10] W.N.N. Hung, X. Song, E.M. Aboulhamid, A. Kennings, and A. Coppola, “Segmented Channel Routability via Satisfiability,” ACM Trans. Design Automation of Electronic Systems, vol. 9, no. 4, pp. 517-528, 2004.
[11] F. He, W.N.N. Hung, X. Song, M. Gu, and J. Sun, “A Satisfiability Formulation for FPGA Routing with Pin Rearrangements,” Int'l J. Electronics, vol. 94, no. 9, pp. 857-868, Sept. 2007.
[12] J.P. Marques-Silva and K.A. Sakallah, “GRASP: A New Search Algorithm for Satisfiability,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD '96), pp. 220-227, Nov. 1996.
[13] L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, “Efficient Conflict Driven Learning in a Boolean Satisfiability Solver,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD), Nov. 2001.
[14] E. Goldberg and Y. Novikov, “BerkMin: A Fast and Robust SAT Solver,” Proc. Design Automation and Test in Europe Conf. Exhibition, pp. 142-149, 2002.
[15] N. Eén and N. Sörensson, “An Extensible Sat-Solver,” Proc. Sixth Int'l Conf. Theory and Applications of Satisability Testing, pp. 502-518, 2003.
[16] B. Selman, H.A. Kautz, and B. Cohen, “Noise Strategies for Improving Local Search,” Proc. 12th Nat'l Conf. Artificial Intelligence (AAAI '94), pp. 337-343, 1994.
[17] B. Selman, H. Levesque, and D. Mitchell, “A New Method for Solving Hard Satisfiability Problems,” Proc. 10th Nat'l Conf. Artificial Intelligence (AAAI), pp. 440-446, 1992.
[18] M. Davis and H. Putnam, “A Computing Procedure for Quantification Theory,” J. ACM, vol. 7, pp. 201-215, 1960.
[19] M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem Proving,” Comm. ACM, vol. 5, pp. 394-397, July 1962.
[20] L. Hai, S. Jigui, and Z. Yimin, “Theorem Proving Based on the Extension Rule,” J. Automated Reasoning, vol. 31, no. 1, pp. 11-21, 2003.
[21] X. Wu, J. Sun, S. Lv, and M. Yin, “Propositional Extension Rule with Reduction,” Int'l J. Computer Science and Network Security, vol. 6, no. 1A, pp. 190-197, Jan. 2006.
[22] P. Cheeseman, B. Kanefsky, and W.M. Taylor, “Where the REALLY Hard Problems Are,” Proc. 12th Int'l Joint Conf. Artificial Intelligence (IJCAI '91), pp. 331-337, 1991.
[23] J.M. Crawford and L.D. Auton, “Experimental Results on the Crossover Point in Satisfiability Problems,” Proc. 11th Nat'l Conf. Artificial Intelligence (AAAI '93), pp. 21-27, 1993.
[24] C. Coarfa, D.D. Demopoulos, A.S.M. Aguirre, D. Subramanian, and M.Y. Vardi, “Random 3-Sat: The Plot Thickens,” Proc. CP '02: Sixth Int'l Conf. Principles and Practice of Constraint Programming, pp. 143-159, 2000.
[25] SATLIB—Benchmark Problems, http://www.cs.ubc.ca/hoos/SATLIBbenchm.html , 2001.
[26] S. Kirkpatrick and B. Selman, “Critical Behavior in the Satisfiability of Random Boolean Expressions,” Science, vol. 264, pp. 1297-1301, 1994.

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:
Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song, Ming Gu, "Maxterm Covering for Satisfiability," IEEE Transactions on Computers, vol. 61, no. 3, pp. 420-426, March 2012, doi:10.1109/TC.2010.270
Usage of this product signifies your acceptance of the Terms of Use.