Inference methods for a pseudo-Boolean satisfiability solver

We describe two methods of doing inference during search 3for 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.