Inference Methods for a Pseudo-Boolean Satisfiability Solver

Heidi E. Dixon and Matthew L. Ginsberg, CIRL / University of Oregon

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.