Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ arXiv.org e-Print Ar...arrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
https://dx.doi.org/10.48550/ar...
Article . 2025
License: arXiv Non-Exclusive Distribution
Data sources: Datacite
versions View all 2 versions
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Introducing Clause Cuts: Strong No-Good Cuts for MaxSAT Problems in Mixed Integer Linear Programming

Authors: Engelhardt, Max; Adhikari, Milan; Staszek, Jonasz; Martin, Alexander;

Introducing Clause Cuts: Strong No-Good Cuts for MaxSAT Problems in Mixed Integer Linear Programming

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 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

Keywords

Optimization and Control (math.OC), Optimization and Control, FOS: Mathematics, 90C10 (Primary), 90C57 (Secondary)

  • BIP!
    Impact byBIP!
    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
Powered by OpenAIRE graph
Found an issue? Give us feedback
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).
BIP!Citations provided by BIP!
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.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Green