State of the art satisfiability solvers provide important tools for problem solving in a number of real world problem domains [44, 10, 18, 60, 42). These methods are all based on the classic DPLL algorithm. Unfortunately, these methods perform poorly on many important families of problems including the pigeonhole problem. Pigeonhole problems state that n + 1 pigeons cannot be placed in n holes and are believed to be common subproblems in many problem domains such as planning and scheduling. The most competitive satisfiability solvers show exponential scaling on these simple structured problems. These problems should be easy but traditional satisfiability methods make them unnecessarily hard.

Traditional satisfiability methods fail to solve these types of problems because the proof system they automate is very weak. The proof system used by traditional methods is resolution and all resolution proofs of the pigeonhole problem are exponential in length [35]. Consequently, traditional methods scale exponentially on pigeonhole problems. The only way to improve performance on these problems is to improve the strength of the underlying representation and inference system. This approach was thought to be impractical because the overhead of managing and automating a stronger and more complex inference system would outweigh any benefits derived from the stronger inference. We implement a DPLL style satisfiability solver that uses pseudo-Boolean representation and automates an inference system properly stronger than resolution. We show that this approach is practical and that in fact, there is no significant advan­tage to resolution based satisfiability methods over their pseudo-Boolean counterpart. Building a pseudo-Boolean solver entails adapting all sub-procedures of a DPLL style method to use pseudo-Boolean representation. We provide an implementation of the learning procedure for pseudo-Boolean constraints and show experimentally that choices made in how learning is implemented determine the strength of the underlying inference system.

We give experimental results showing that the pseudo-Boolean solver can always closely match the performance of traditional methods yet the reverse is not true. The pseudo-Boolean solver allows exponential speedups over traditional methods on pigeonhole problems. We also give experimental results showing that traditional methods are unnecessarily slow on random planning problems due to embedded pigeonhole problems.