Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems
Richard J. Wallace, Eugene C. Freuder · DIMACS series in discrete mathematics and theoretical computer science · 1996
Maximum satisfiability (MAX-SAT) is an extension of satisfiability (SAT), in which a partial solution is sought that satisfies the maximum number of clauses in a logical formula. Enumerative methods giving guaranteed optimal solutions can be derived from traditional search algorithms used to solve SAT problems, in particular the Davis- Putnam procedure. Algorithms have also been developed for the maximal constraint satisfaction problem (MAX-CSP), a generalization of MAX-SAT, that are extensions of search algorithms used to solve constraint satisfaction problems. In the present work, these algorithms were compared over the same sets of problems, using comparable implementations. In addition, variants of each algorithm were tested to determine the contribution of component strategies that often make up a working algorithm. The componential analysis was done using traditional multi-factor experimental designs in which the effect of different strategies could be studied at the same time th...