Clustering and partition based divide and conquer for SAT solving

被引：0

作者：

Fan, Quan-Run ^{[1
]}

Duan, Zhen-Hua ^{[1
,2
]}

机构：

[1] Institute of Computing Theory and Technology, Xidian University, Xi'an

[2] State Key Laboratory of Integrated Services Networks, Xidian University, Xi'an

来源：

Ruan Jian Xue Bao/Journal of Software | 2015年 / 26卷 / 09期

关键词：

Boolean satisfiability; Clustering; Conjunctive normal form; Partition;

D O I：

10.13328/j.cnki.jos.004799

中图分类号：

学科分类号：

摘要：

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. © Copyright 2015, Institute of Software, the Chinese Academy of Sciences. All right reserved.

引用

页码：2155 / 2166

页数：11

共 26 条

[1]

Cook S., The complexity of theorem proving procedures, Proc. of the ACM SIGACT Symp. on the Theory of Computing, (1971)

[2]

Tseitin G., On the complexity of derivation in propositional calculus, Proc. of the Structures in Constructive Mathematics and Mathematical Logic, Part II: Seminars in Mathematics, pp. 115-125, (1968)

[3]

Impagliazzo R., Paturi R., Zane F., Which problems have strongly exponential complexity?, Journal of Computer and System Sciences, 63, 4, pp. 512-530, (2001)

[4]

Calabro C., Impagliazzo R., Paturi R., A duality between clause width and clause density for sat, Proc. of the 21st Annual IEEE Conf. on Computational Complexity, pp. 252-260, (2006)

[5]

Impagliazzo R., Paturi R., On the complexity of k-SAT, Journal of Computer and System Sciences, 62, 2, pp. 367-375, (2001)

[6]

Een N., Biere A., Effective preprocessing in SAT through variable and clause elimination, Proc. of the 8th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2005), pp. 61-75, (2005)

[7]

Jarvisalo M., Biere A., Heule M., Simulating circuit-level simplifications on CNF, Journal of Automated Reasoning, 49, 4, pp. 583-619, (2012)

[8]

Handbook of Satisfiability, (2009)

[9]

Davis M., Logemann G., Loveland D., A machine program for theorem proving, Communications of the ACM, 5, 7, pp. 394-397, (1962)

[10]

Marques-Silva J., Sakallah K., GRASP: A search algorithm for propositional satisfiability, IEEE Trans. on Computers, 48, 5, pp. 506-521, (1999)

← 1 2 3 →