214. Introducing clause-cuts to speed up MaxSAT problems in mixed integer linear programming
Invited abstract in session TD-2: Integer Programming II, stream Discrete and Combinatorial Optimization.
Thursday, 14:30-16:00Room: H4
Authors (first author is the speaker)
| 1. | Max Engelhardt
|
| University of Technology Nuremberg | |
| 2. | Milan Adhikari
|
| University of Technology Nuremberg | |
| 3. | Jonasz Staszek
|
| Technische Universität Nürnberg | |
| 4. | Alexander Martin
|
| Liberal Arts and Sciences, University of Technology Nuremberg (UTN) |
Abstract
In this paper we introduce clause-cuts: linear inequalities obtained from clauses that are logically implied by a CNF formula, resembling strengthened no-good-cuts. With these cuts, we tighten mixed-integer linear programming (MILP) formulations of random weighted partial MAXSAT-problems, which have remained particularly challenging for MAXSAT-solvers. Our approach derives cuts from the set of variables that attain integral values at the LP relaxation, using SAT solvers to evaluate the feasibility of these partial assignments. When infeasible, these assignments are ruled out with clause-cuts which are further strengthened with the SAT-solver. Two separation algorithms are introduced, one that utilizes a SAT-oracle, and another that uses the clauses learned by a conflict driven clause learning (CDCL) SAT-solver. Experiments on SATLIB benchmarks demonstrate substantial performance gains – up to two orders of magnitude – compared to the general purpose MILP-solver Gurobi 12 and surpass the specialized MAXSAT-solver RC2. We explain the source of these gains and the limitations of standard MILP formulations in this context.
Keywords
- Integer Programming
- Constraint Programming
- Linear Programming
Status: accepted
Back to the list of papers