
arXiv: 2509.21687
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 core-guided complete MaxSAT solvers. Our approaches treat variables that attain integral values at the LP relaxation as partial assignments which are supplied to a SAT solver as assumptions. 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 finds Clause Cuts in the set of variables with integral values, and another that uses the clauses learned by a conflict driven clause learning (CDCL) SAT solver while evaluating the partial assignment. Experiments on SATLIB benchmarks demonstrate substantial performance gains of up to two orders of magnitude compared to the general purpose MILP solver Gurobi 12, taking only 7.8% of Gurobi's runtime for the whole problem set. Results also surpass the specialized MaxSAT solver RC2, taking only 60% of its runtime. In some cases, our optimization takes only slightly longer than a single SAT call on the SAT-formula. We explain the source of these gains and the limitations of standard MILP formulations in this context.
21 pages, 9 figures
Optimization and Control (math.OC), Optimization and Control, FOS: Mathematics, 90C10 (Primary), 90C57 (Secondary)
Optimization and Control (math.OC), Optimization and Control, FOS: Mathematics, 90C10 (Primary), 90C57 (Secondary)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
