Enhancing maximum satisfiability algorithms with pure literal strategies

Abstract

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. In recent years there has been an growing interest in this and other types of over-constrained problems. Branch and bound extensions of the Davis-Putnam algorithm can return guaranteed optimal solutions to these problems. Earlier work did not make use of a pure literal rule because it appealed to be inefficient here, as for traditional SAT. However, arguments can be adduced to show that pure literals are likely to appear during search for MAX-2SAT, so that fixation of their variables may be effective here. The present work confirms this and also shows that a value ordering heuristic involving literals that are monotone in unit open clauses can be very effective, operating somewhat independently of the ordinary fixation of fully monotone literals. Alone or together, these pure literal strategies can produce improvements of an order of magnitude or more when combined with versions of Davis-Putnam studied in earlier work, sometimes solving problems of considerable size.

This material is based on work supported by the National Science Foundation under Grant Nos. IRI-9207633 and IRI-9504316.