Solving Linear Pseudo-Boolean Co
Joachim R Walses · 1997
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 (O-l integer) constraints, a representation that is widely used in operations research. We introduce the algorithm W SAT (%‘B) 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 (PI?) 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 O-l encoding is beyond the size limitations of integer linear programming. Local search is versatile and many successful applications of domain-specific local search methods have been reported. Further, a number of successful domainindependent methods exist that include strategies for maximum satisfiability (Hansen & Jaumard 1990), for certain realistic constraint satisfaction (CSP) problems (Minton et al. 1990; Hao & Dorne 1996), and some of the most efficient methods for hard realistic and randomly generated propositional satisfiability (SAT) problems (Selman,