MAXSAT, A Davis-Putnam like code for MAX-SAT Problems

This page contains links to the code and test problems from

Brian Borchers and Judith Furman, A Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems, Journal of Combinatorial Optimization. 2(4): 299-306, 1999.

Note that the code was updated on March 26, 1998 to correct a minor bug- the code wasn't properly handling clauses in which literals were repeated.

An important note: these codes all assume that each variable is present in at least one clause in the SAT problem. If you have a problem in which some variable is not present in any clause, then you can either rename the variables to avoid this, or add a clause to the effect that either the variable or its negation must be true.

Return to Brian Borchers Homepage