Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Integer Linear Programming Preprocessing for Maximum Satisfiability

Jialu Zhang, Chu-Min Li, Sami Cherif, Shuolin Li, Zhifei Zheng

TL;DR

MaxSAT is analyzed as an optimization over CNF with hard clauses $H$ and soft clauses $S$, and the paper proposes a three-stage pipeline to integrate ILP preprocessing: build an ILP model from the MaxSAT instance, apply SCIP preprocessing to obtain a simplified model, and re-encode it to CNF for solving, followed by reconstruction of the original solution. The approach reduces problem size without relying on fixed ILP time budgets, enabling improvements across top MaxSAT solvers and reducing the need for lengthy portfolio calls. Experimental results on MS/WMS datasets show substantial reductions in variables and clauses in many instances and performance gains for 5 of 6 state-of-the-art solvers, including 15 extra solves for WMaxCDCL-OpenWbo1200. The work demonstrates that ILP preprocessing can be effectively embedded in MaxSAT pipelines, with future work aimed at stronger encoding methods and identifying the most impactful ILP techniques to further enhance preprocessing efficiency.

Abstract

The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.

Integer Linear Programming Preprocessing for Maximum Satisfiability

TL;DR

MaxSAT is analyzed as an optimization over CNF with hard clauses and soft clauses , and the paper proposes a three-stage pipeline to integrate ILP preprocessing: build an ILP model from the MaxSAT instance, apply SCIP preprocessing to obtain a simplified model, and re-encode it to CNF for solving, followed by reconstruction of the original solution. The approach reduces problem size without relying on fixed ILP time budgets, enabling improvements across top MaxSAT solvers and reducing the need for lengthy portfolio calls. Experimental results on MS/WMS datasets show substantial reductions in variables and clauses in many instances and performance gains for 5 of 6 state-of-the-art solvers, including 15 extra solves for WMaxCDCL-OpenWbo1200. The work demonstrates that ILP preprocessing can be effectively embedded in MaxSAT pipelines, with future work aimed at stronger encoding methods and identifying the most impactful ILP techniques to further enhance preprocessing efficiency.

Abstract

The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.

Paper Structure

This paper contains 13 sections, 1 equation, 3 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Maximum Satisfiability
  4. Preprocessing Techniques
  5. Methodology
  6. Integrating ILP Preprocessing into MaxSAT Solving
  7. Variable Encoding
  8. Constraint Encoding
  9. Experimental Results
  10. Experimental Protocol
  11. Impact of ILP Preprocessing
  12. Performance of MaxSAT solvers
  13. Conclusion

Figures (3)

  • Figure 1: Pipeline of the three-stage methodology
  • Figure 2: Comparison between $originInst$ (vertical axes) and $simpInst$ (horizontal axes) in terms of variables, clauses, and the sum of soft weights. The axes are on a logarithmic scale.
  • Figure 3: Number of solved instances changes with solving time (in seconds). Solid lines in the subfigures represent the baseline solvers, and the dashed lines represent the baseline solvers with ILP preprocessing (+simp).