Inference Methods for a Pseudo-Boolean Satisfiability Solver

Abstract

We describe two methods of doing inference during search for a pseudo-Boolean version of the RELSAT method. One inference method is the pseudo-Boolean equivalent of learning. A new constraint is learned in response to a contradiction with the purpose of eliminating the set of assignments that caused the contradiction. We show that the obvious way of extending learning to pseudo-Boolean is inadequate and describe a better solution. We also describe a second inference method used by the Operations Research community. The method cannot be applied to the standard resolution-based AI algorithms, but is useful for pseudo-Boolean versions of the same AI algorithms. We give experimental results showing that the pseudo-Boolean version of RELSAT outperforms its clausal counterpart on problems from the planning domain.