PBS: A backtrack search pseudo Boolean solver

in areas such as hardware and software verification, FPGA routing, planning in AI, etc. Further uses are complicated by the need to express “counting constraints ” in conjunctive normal form (CNF). Expressing such constraints by pure CNF leads to more complex SAT instances. Alternatively, those constraints can be handled by Integer Linear Programming (ILP), but off-the-shelf ILP solvers tend to ignore the Boolean nature of 0-1 variables. This work attempts to generalize recent highly successful SAT techniques to new applications. First, we extend the basic Davis-Putnam framework to handle counting constraints and apply it to solve routing problems. Our implementation outperforms previously reported solvers for the satisfiability with “pseudo-Boolean ” constraints and shows significant speed-up over best SAT solvers when such constraints are translated into CNF,. Additionally, we solve instances of the Max-ONEs optimization problem which seeks to maximize the number of “true ” values over all satisfying assignments. This, and the related Min-ONEs problem are important due to reductions from Max-Clique and Min Vertex Cover. Our experimental results for various benchmarks are superior to all approaches reported earlier.