PB-Smodels a Pseudo-Boolean Solver

Abstract

A pseudo-boolean constraint (PB-constraint) is a linear inequality with 0-1 variables and integer coefficients. Search problems can be modeled as sets of PB-constraints, so that, solutions to a set of PB-constraints map to solutions of the search problem. An optimization problem can be modeled using a set of PB-constraints along with an optimization statement over a set of 0-1 variables. Pseudo-boolean solvers (PB-solvers) are programs designed to find solutions to a set of PB-constraints, and hence can be used to solve search problems. PBS4 (Aloul 2005), MiniSat+ (Een & Sorensson 2005), BSOLO (Manquinho & Marques-Silva 2005) and Pueblo (Sheini & Sakallah 2005) are recent PB-solvers. Our contribution is to show that smodels, a solver originally designed to solve search problems encoded as logic programs with weight constraints (Niemela & Simons 1997), can be used as a competitive PB-solver. We call this PB-solver PB-smodels. PB-smodels uses a procedure we designed, PB2smodels, to translate a set of PB-constraints into a logic program that is accepted by smodels. We show that solutions of a search problem modeled as a set of PB-constraints T correspond to stable models of the logic program P (T ) produced from T by PB2smodels. We compare the performance of PB-smodels with two PB-solvers MiniSat+ and Pueblo on search problems encoded as sets of PB-constraints. In particular, we compare PB-smodels to MiniSat+ and Pueblo on benchmarks obtained from PB 2005 competition (Manquinho & Roussel 2006). We also compare the PB-solvers on benchmarks derived from randomly generated instances of problems such as weighted N-queens, traveling salesperson problem (TSP), blocked N-queens and weighted dominating set problem.