Stochastic local search is one of the most successful methods for model finding in propositional satisfiability. However, many combinatorial problems have no concise propositional encoding. In this paper, we show that domain-independent local search for satisfiability (Walksat) can be generalized to handle systems of linear pseudo-Boolean (0-1 integer) constraints, a representation that is widely used in operations research. We introduce the algorithm WSAT(PB) and demonstrate its potential in two case studies. The first application is an optimization problem from radar surveillance. Experiments on problems of realistic size show that WSAT(PB) is an efficient heuristic to find good approximate solutions. For most of the test problems, it found provably optimal solutions. In the second case study, we show that pseudo-Boolean local search can efficiently solve the progressive party problem, a problem that is hard for constraint programming with chronological backtracking, and whose 0-1 encoding is beyond the size limitations of integer linear programming.
Download PDF Show BibTeX
Login to edit