Clone is a branch-and-bound Max-SAT solver which uses a novel approach for computing bounds by making use of a tractable language known as d-DNNF. A problem instance is first compiled into d-DNNF form using a program called c2d. Once in d-DNNF form, a Max-SAT problem can then be solved effeciently in polynomial time. However, when dealing with problems having large treewidths, a method known as variable splitting is first employed in order to relax the original problem instance. As a result of this relaxation process, the solution to the relaxed problem is only a bound for the solution to the original problem. This bound computation method is utilized by a branch-and-bound solver in order to find the optimal solution. One key advantage of this approach is that the solver only needs to branch on split variables (as opposed to all the variables).
For more information, please refer to the following papers:
Pipatsrisawat, K., Palyan, A., Chavira, M., Choi, A., and Darwiche A. Solving Weighted Max-SAT in a Reduced Search Space: A Performance Analysis. Journal on Satisfiability Boolean Modeling and Computation (JSAT), Volume 4 (2008), pages 191-217. [BIB]
Pipatsrisawat, K. and Darwiche, A. Clone: Solving Weighted Max-SAT in a Reduced Search Space. In proceedings of 20th Australian Joint Conference on Artificial Intelligence, Queensland, Australia, December 2007. [BIB]
Clone participated in the 2008 Max-SAT Evaluation in the weighted, partial, and weighted partial categories. All problem instances were in the extended DIMACS CNF format.
Download Clone and random benchmark problems.
Clone utilizes a modified version of MaxWalksat, a stochastic local search Max-SAT solver, which is included with the download package above. For more information on MaxWalksat, refer to the Walksat Home Page.
Send questions and comments to clone at cs.ucla.edu.