Enhancing Maximum Satisfiability Algorithms with Pure Literal Strategies

. 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 appeared 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 i..