Automating pseudo-boolean inference within a dpll framework
H. E. Dixon, Matthew L. Ginsberg, Christopher B. Wilson · 2004
State of the art satisfiability solvers provide important tools for problem solving in a number of real world problem domains. 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 if each gets its own hole. They 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 traditionalv methods is resolution and all resolution proofs of the pigeonhole problem are exponential in length. Consequently, traditional methods scale exponentially on pigeonhole problems. The only way to improve performance on these problems is to improve