Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems.

*(English)*Zbl 0859.68072
Johnson, David S. (ed.) et al., Cliques, coloring, and satisfiability. Second DIMACS implementation challenge. Proceedings of a workshop held at DIMACS, October 11–13, 1993. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 26, 587-615 (1996).

Summary: 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 that problem parameters were varied. Most of this work was done with MAX-2SAT problems, although Davis-Putnam variants were also tested with MAX-3SAT.

The performance of Davis-Putnam on MAX-SAT problems depended heavily on the combination of strategies used, and the superiority of a particular combination also depended on problem characteristics. In particular, the clause: variable ratio was shown to be an important determinant of relative performance. The best MAX-CSP algorithms were competitive with Davis-Putnam in this domain, but relative performance depended, again, on problem parameters.

For the entire collection see [Zbl 0851.00080].

The performance of Davis-Putnam on MAX-SAT problems depended heavily on the combination of strategies used, and the superiority of a particular combination also depended on problem characteristics. In particular, the clause: variable ratio was shown to be an important determinant of relative performance. The best MAX-CSP algorithms were competitive with Davis-Putnam in this domain, but relative performance depended, again, on problem parameters.

For the entire collection see [Zbl 0851.00080].

##### MSC:

68R99 | Discrete mathematics in relation to computer science |

68Q25 | Analysis of algorithms and problem complexity |

05A99 | Enumerative combinatorics |

00B25 | Proceedings of conferences of miscellaneous specific interest |