微信服务号

微信订阅号

2025-5-15- 15
Home > Archive>Volume 26, Issue 9, 2015 >2155-2166. DOI:10.13328/j.cnki.jos.004799
PDF HTML XML Export Cite reminder
Clustering and Partition Based Divide and Conquer for SAT Solving
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [26]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    A partition based Boolean satisfiability solving method is proposed. By partitioning a CNF(conjunctive normal form) formula into several clause groups, Boolean satisfiability problem can be divided into small sub-problems, hence reducing the complexity of the original problem. Meanwhile, the satisfiability of different clause group can be solved in parallel, thus further speeding up the decision procedure. For the formula that clause group partition cannot be generated directly, a clustering algorithm is given to cluster clauses into clusters so that clause group partition can be generated by eliminating common variables among clusters.

    Reference
    [1] Cook S. The complexity of theorem proving procedures. In: Proc. of the ACM SIGACT Symp. on the Theory of Computing. 1971. [doi: 10.1145/800157.805047]
    [2] Tseitin. G. On the complexity of derivation in propositional calculus. In: Proc. of the Structures in Constructive Mathematics and Mathematical Logic, Part II: Seminars in Mathematics (translated from Russian). Steklov Mathematical Institute, 1968. 115-125. [doi: 10.1007/978-3-642-81955-1_28]
    [3] Impagliazzo R, Paturi R, Zane F. Which problems have strongly exponential complexity? Journal of Computer and System Sciences, 2001,63(4):512-530. [doi: 10.1006/jcss.2001.1774]
    [4] Calabro C, Impagliazzo R, Paturi R. A duality between clause width and clause density for sat. In: Proc. of the 21st Annual IEEE Conf. on Computational Complexity. Washington: IEEE Computer Society, 2006. 252-260. [doi: 10.1109/CCC.2006.6]
    [5] Impagliazzo R, Paturi R. On the complexity of k-SAT. Journal of Computer and System Sciences, 2001,62(2):367-375. [doi: 10.1006/jcss.2000.1727]
    [6] Eén N, Biere A. Effective preprocessing in SAT through variable and clause elimination. In: Proc. of the 8th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2005). LNCS 3569, 2005. 61-75. [doi: 10.1007/11499107_5]
    [7] Järvisalo M, Biere A, Heule M. Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning, 2012,49(4): 583-619. [doi: 10.1007/s10817-011-9239-9]
    [8] Biere A, Heule M, Maaren H, Walsh T, eds. Handbook of Satisfiability. IOS Press, 2009. [doi: 10.3233/978-1-58603-929-5-3]
    [9] Davis M, Logemann G, Loveland D. A machine program for theorem proving. Communications of the ACM, 1962,5(7):394-397. [doi: 10.1145/368273.368557]
    [10] Marques-Silva J, Sakallah K. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Computers, 1999,48(5): 506-521. [doi: 10.1109/12.769433]
    [11] Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S. Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conf. (DAC 2001). 2001. 530-535. [doi: 10.1145/378239.379017]
    [12] Goldberg E, Novikov Y. Berkmin: A fast and robust SAT solver. In: Proc. of the 5th Design Automation and Test in Europe (DATE 2002). 2002. 142-149. [doi: 10.1016/j.dam.2006.10.007]
    [13] Sörensson N, Eén N. MiniSat V1.13—A SAT solver with conflict-clause minimization. In: Proc. of the Posters of the Int'l Symp. on the Theory and Applications of Satisfiability Testing (SAT 2005). 2005.
    [14] Audemard G, Simon L. Predicting learnt clauses quality in modern SAT Solver. In: Proc. of the 21st Int'l Joint Conf. on Artificial Intelligence (IJCAI 2009). 2009.
    [15] Durairaj V, Kalla P. Guiding CNF-SAT search by analyzing constraint-variable dependencies and clause lengths. In: Proc. of the High-Level Design Validation and Test Workshop (HLDVT). 2006. 155-161. [doi: 10.1109/HLDVT.2006.319983]
    [16] Durairaj V, Kalla P. Exploiting hypergraph partitioning for efficient Boolean satisfiability. In: Proc. of the 9th IEEE Int High Level Design Validation and Test Workshp. 2004. [doi: 10.1109/HLDVT.2004.1431257]
    [17] Cai SW, Su KL, Sattar A. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artificial Intelligence, 2011,175(9-10):1672-1696. [doi: 10.1016/j.artint.2011.03.003]
    [18] Cai SW, Su KL. Configuration checking with aspiration in local search for SAT. In: Proc. of the AAAI 2012. 2012.
    [19] Cai SW, Su KL. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013,204: 75-98. [doi: 10.1016/j.artint.2013.09.001]
    [20] Samulowitz H, Bacchus F. Dynamically partitioning for solving QBF. In: Proc. of the 10th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2007). 2007. 215-229. [doi: 10.1007/978-3-540-72788-0_22]
    [21] Hyvärinen A, Junttila T, Niemelä I. Partitioning SAT instances for distributed solving. In: Proc. of the Int'l Conf. on Logic for Programming, Artificial Intelligence, and Reasoning. LNCS 6397, 2010. 372-386. [doi: doi=10.1.1.174.6279]
    [22] Estivill-Castro V. Why so many clustering algorithms? ACM SIGKDD Explorations Newsletter, 2002,4(1):65-75. [doi: 10.1145/ 568574.568575]
    [23] CNF file format. 2013. http://people.sc.fsu.edu/~jburkardt/pdf/dimacs_cnf.pdf
    [24] Hoos H, Stützle T. SATLIB: An online resource for research on SAT. In: Gent IP, Maaren HV, Walsh T, eds. Proc. of the SAT 2000. IOS Press, 2000. 283-292.
    [25] sc13-Benchmarks-Application. 2013. http://www.satcompetition.org/2013/files/sc13-benchmarks-application.tgz
    [26] Biere A. Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Balint A, Belov A, Heule M, Järvisalo M, eds. Proc. of the SAT Competition 2013. vol.B-2013-1 of Department of Computer Science Series of Publications B, University of Helsinki, 2013. 51-52.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

范全润,段振华.基于聚类和划分的SAT分治判定.软件学报,2015,26(9):2155-2166

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 03,2014
  • Revised:October 21,2014
  • Online: September 14,2015
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044671Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063