A Decision-Making Procedure for Resolution-Based SAT-Solvers
We describe a new decision-making procedure for resolution-based SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference po
- PDF / 459,282 Bytes
- 14 Pages / 430 x 660 pts Page_size
- 32 Downloads / 159 Views
Abstract. We describe a new decision-making procedure for resolutionbased SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference point under which the number of clauses falsified by the modified point is smaller than for the original one. DMRP makes it possible for a DPLLlike algorithm to perform a ”local search strategy”. We describe a SATalgorithm with conflict clause learning that uses DMRP. Experimental results show that even a straightforward and unoptimized implementation of this algorithm is competitive with SAT-solvers like BerkMin and Minisat on practical formulas. Interestingly, DMRP is beneficial not only for satisfiable but also for unsatisfiable formulas.
1
Introduction
Resolution based SAT-solvers have gained great popularity due to their ability to solve very large practical CNF formulas. An important contributor to this success is conflict driven decision making (CDDM) introduced in [17] and further developed in BerkMin [7], Minisat [3], Siege and other SAT-solvers. CDDM takes into account the history of conflicts thus forcing the SAT-solver to explore the parts of the search space that have not been visited before. Despite the obvious success of CDDM, still there are many directions to explore. In this paper, we introduce a resolution based SAT-solver whose decision making procedure employs a complete assignment further referred to as a reference point. We will refer to this procedure as Decision Making with a Reference Point (DMRP). (We will refer to the SAT-solver employing DMRP that we describe in this paper as DMRP-SAT.) The main idea of DMRP is as follows. Let F be the CNF formula to be solved. Let p be a reference point and M (p) be the set of clauses of F that are falsified by p. DMRP-SAT picks a clause C of M (p) and tries to find a modification p of p that satisfies C and does not falsify any clauses of F that are not in M (p) \ {C}. In other words, M (p ) ⊂ M (p). Importantly, the search of the point p above is done by a regular DPLLlike procedure with conflict clause learning. After p is found, it becomes a new H. Kleine B¨ uning and X. Zhao (Eds.): SAT 2008, LNCS 4996, pp. 119–132, 2008. c Springer-Verlag Berlin Heidelberg 2008
120
E. Goldberg
reference point and DMRP-SAT performs a complete restart. In our previous paper [6], we described the resolution-based SAT-solver called FI that operates on complete assignments. One can view the decision making procedure of FI as a variation of CDDM. Similarly to CDDM and decision making of FI, DMRP also gives some preference to recently derived conflict clauses. At the same time, DMRP is not just a variation of CDDM. DMRP makes it possible for a SAT-solver to monotonically reduce the number of clauses falsified by the current reference point. So, in a sense, DMRP-SAT combines the features of algorithms based on the DPLL procedure [2] and local search SAT-algorithms pioneered in [20,21]. The strategy of reducing the numb
Data Loading...
