Oracle-Based Local Search for Pseudo-Boolean Optimization

Significant advances have been recently made in the development of increasingly effective in-exact (or incomplete) search algorithms---particularly geared towards finding good though not provably optimal solutions fast---for the constraint optimization paradigm of maximum satisfiability (MaxSAT). One of the most successful recent approaches is a new type of stochastic local search in which---to an extent counterintuitively---a Boolean satisfiability (SAT) solver is used as a decision oracle for moving from a solution to another. In this work, we strive for extending the success of the approach to the more general realm of pseudo-Boolean optimization (PBO), where constraints are expressed as linear inequalities over binary variables. As a basis for the approach, we make use of recent advances in practical approaches to satisfiability checking pseudo-Boolean constraints. We outline various heuristics within the oracle-based approach to anytime PBO solving, and show that the approach compares in practice favourably both to a recently-proposed local search approach for PBO that is in comparison a more traditional instantiation of the stochastic local search paradigm, and a recent exact PBO approach when used as an anytime solver.