Incomplete Dynamic Backtracking for Linear Pseudo-Boolean Problems

Many combinatorial problems can be modeled as 0/1 integer linear programs. Problems expressed in this form are usually solved by Operations Research algorithms, but good results have also been obtained using generalised SAT algorithms based on backtracking or local search, after transformation to pseudo-Boolean form. A third class of SAT algorithm uses non-systematic backtracking to combine constraint propagation with local search-like scalability, at the cost of completeness. This paper describes such an algorithm for pseudo-Boolean models. Experimental results on a variety of problems are encouraging, in some cases yielding improved solutions or performance compared to previous algorithms.