Satisfiability-based algorithms for pseudo-Boolean optimization using Gomory cuts and search restarts

Cutting planes are a well-known, widely used, and very effective technique for integer linear programming (ILP). In contrast, the utilization of cutting planes in pseudo-Boolean Optimization (PBO) is recent and results still preliminary. This paper addresses the utilization of cutting planes, namely Gomory mixed-integer cuts, in satisfiability-based algorithms for PBO, and shows how these cuts can be used for computing lower bounds and for learning new constraints. A side result of learning new constraints is that the utilization of cutting planes enables non-chronological backtracking. Besides cutting planes, the paper also proposes the utilization of search restarts in PBO. We show that search restarts can be effective in practice, allowing the computation of more aggressive lower bounds each time the search restarts. Experimental results show that the integration of cutting planes and search restarts in a SAT-based algorithm for PBO yields a very efficient and robust new solution for PBO