A New Branch and Bound Method for Incremental Satisfiability Problem.
Malek Mouhoub, Samira Sadaoui, Xinkai Feng · International Conference on Computational Intelligence · 2004
We present in this paper a new method based on branch and bound for solving the incremental satisfiability (SAT) problem. More precisely, the goal of the method is to maintain, in an incremental manner, the satisfiability of a given boolean formula in Conjunctive Normal Form (CNF) anytime a new set of clauses is added. Solving incremental SAT is very appealing for a wide variety of real-life combinatorial applications such as online scheduling and planning, robot motion planning, network routing and transportation scheduling. We will show that the branch and bound algorithm can be improved by taking advantage of the structure of the CNF formula. Experimental study, on randomly generated SAT instances taken from the well known SAT library, demonstrates the efficiency of our method especially for large SAT problems. KeywordsBoolean Satisfiability, Branch and Bound, Local Search.