Source-linked AI summary
Algorithms for Weighted Boolean Optimization
Vasco Manquinho, Joao Marques-Silva, Jordi Planes
TL;DR
MaxSAT and PBO have straightforward mappings but developed separate algorithms, motivating a unified treatment. The paper introduces WBO and extends unsatisfiability-based MaxSAT solving to it. Experiments show that weighted MaxSAT can outperform existing algorithms by orders of magnitude, while a general WBO algorithm can match dedicated solvers.
Problem
MaxSAT and PBO evolved separately despite straightforward mappings between them, leaving a need for a unified framework and broader unsatisfiability-based methods.
Method
The paper introduces WBO and extends unsatisfiability-based weighted MaxSAT algorithms to solve WBO using native pseudo-Boolean solving or clausal translation.
Results
Weighted MaxSAT can outperform existing algorithms by orders of magnitude, and a general WBO algorithm can be as efficient as dedicated algorithms.
Takeaways & Limitations
Integrating MaxSAT and PBO provides a common optimization extension of SAT and supports general-purpose algorithms combining techniques from both domains.
Takeaways & Limitations
The experimental comparison is preliminary and possibly biased, and observed differences may also reflect the different underlying SAT solvers.
Abstract
from arXiv · showhide
The Pseudo-Boolean Optimization (PBO) and Maximum Satisfiability (MaxSAT) problems are natural optimization extensions of Boolean Satisfiability (SAT). In the recent past, different algorithms have been proposed for PBO and for MaxSAT, despite the existence of straightforward mappings from PBO to MaxSAT and vice-versa. This papers proposes Weighted Boolean Optimization (WBO), a new unified framework that aggregates and extends PBO and MaxSAT. In addition, the paper proposes a new unsatisfiability-based algorithm for WBO, based on recent unsatisfiability-based algorithms for MaxSAT. Besides standard MaxSAT, the new algorithm can also be used to solve weighted MaxSAT and PBO, handling pseudo-Boolean constraints either natively or by translation to clausal form. Experimental results illustrate that unsatisfiability-based algorithms for MaxSAT can be orders of magnitude more efficient than existing dedicated algorithms. Finally, the paper illustrates how other algorithms for either PBO or MaxSAT can be extended to WBO.
1 Introduction
MaxSAT and PBO extend SAT for optimization, but their algorithms evolved separately despite straightforward translations between the formalisms. The paper addresses this separation by extending unsatisfiability-based methods and introducing a unified framework.
- Motivation: MaxSAT and PBO are natural optimization extensions of SAT with straightforward translations between them.Nevertheless, their algorithms often use fairly different organizations.
- Motivation: Unsatisfiability-based approaches had expanded solving alternatives but remained restricted to selected MaxSAT and PBO variants.The paper identifies these restrictions as a motivation for broader methods.
- Contributions: The paper proposes a simple unsatisfiability-based algorithm for Partial Weighted MaxSAT.
- Contributions: Weighted Boolean Optimization generalizes MaxSAT and PBO as a framework for linear optimization over Boolean domains.
- Contributions: The paper extends unsatisfiability-based MaxSAT algorithms to WBO and reports that such solvers can outperform state-of-the-art solvers on practical instances.
2 Preliminaries
The preliminaries define MaxSAT and PBO, describe their variants and solving approaches, and explain translations between them. They also introduce unsatisfiability-based MaxSAT algorithms used later in the paper.
- MaxSAT: MaxSAT maximizes satisfied clauses, while weighted MaxSAT minimizes the total weight of unsatisfied clauses.
- MaxSAT: Partial MaxSAT requires all hard clauses to be satisfied while maximizing the number of satisfied soft clauses.
- MaxSAT: Weighted partial MaxSAT combines weighted soft clauses with classical hard clauses, with hard clauses also representable through sufficiently large weights.
- PBO: PBO optimizes a linear objective subject to linear inequalities with integer coefficients over Boolean variables.
- PBO: PBO solvers commonly use SAT techniques, objective-value search, branch and bound, native pseudo-Boolean reasoning, or clause encodings.
- Translations: MaxSAT and PBO can encode into each other: soft clauses use selection variables in PBO, while PBO constraints become hard clauses and objective terms become weighted soft clauses in MaxSAT.
- Unsatisfiability-Based MaxSAT: Unsatisfiability-based MaxSAT algorithms iteratively identify and relax unsatisfiable sub-formulas using SAT solvers.
3 Unsatisfiability-Based Weighted MaxSAT
The weighted MaxSAT algorithm extends MSU-style unsatisfiability-based solving by handling clause weights through splitting and relaxation. It collapses repeated work associated with large weights while preserving optimality.
- Weighted MaxSAT: Replicating a weighted clause according to its weight is correct but scales poorly when weights are large.An unsatisfiable sub-formula with smallest weight minc would be identified minc times.
- Weighted MaxSAT: The improved algorithm splits clauses only when they occur in an unsatisfiable sub-formula and computes its smallest clause weight minc.
- Weighted MaxSAT: Clauses heavier than minc are split into a relaxed clause of weight minc plus a residual clause with reduced weight.
- Weighted MaxSAT: The algorithm collapses minc iterations of the naive weighted approach into one iteration, which can significantly help for large clause weights.
- Correctness: Theorem: WMSU1 returns the minimum cost of non-satisfied clauses.
4 Weighted Boolean Optimization
Weighted Boolean Optimization (WBO) unifies MaxSAT and PBO by allowing weighted soft and hard pseudo-Boolean constraints. Its unsatisfiability-based solver extends weighted MaxSAT reasoning to pseudo-Boolean formulas, including compact relaxation techniques.
- WBO framework: WBO is a unified framework containing weighted soft and hard pseudo-Boolean constraints, extending both MaxSAT variants and PBO.Hard constraints must hold, while the weighted cost of unsatisfied soft constraints is minimized.
- Unsatisfiability-based algorithm: The WBO solver replaces the SAT solver with a pseudo-Boolean solver that can generate an unsatisfiable sub-formula from the original formula.The remaining unsatisfiability-based weighted MaxSAT procedure is adapted to pseudo-Boolean constraints.
- Unsatisfiability-based algorithm: When a soft pseudo-Boolean constraint is relaxed, a fresh variable is added to its left-hand side, producing a constraint such as ωR = b · r + P ajlj ≥b.The relaxation variable permits the constraint to be violated while preserving the pseudo-Boolean form.
- Unsatisfiability-based algorithm: The constraint requiring exactly one selected relaxation variable can be added directly as a pseudo-Boolean constraint, avoiding CNF encoding and often producing a more compact formulation.This is especially useful when an unsatisfiable core contains many soft constraints.
- Relaxation-variable reduction: Some unsatisfiable cores need fewer relaxation variables than soft constraints because pairs of constraints cannot be violated simultaneously.Such sharing is represented through a maximum-cardinality matching problem, and the paper gives examples reducing four variables to two.
- Alternative approaches: Alternative WBO approaches extend PBO or branch-and-bound MaxSAT solvers, but they respectively inherit potential drawbacks or refine upper bounds rather than lower bounds.The proposed Section 4.1 algorithm instead refines lower bounds on the optimum value.
5 Results
Experiments on industrially motivated instances compared weighted MaxSAT, PBO, and WBO solvers under fixed resource limits. The results show strong solver specialization, with MSUnCore, WBO, and IncWMaxSatz solving all IND instances and MSUnCore leading overall among the selected solvers.
- Overall solver performance: Only a small number of MaxSAT solvers was effective on practical problem instances, while PBO solvers were competitive on different instance classes.The IND benchmarks were challenging for PBO solvers because of their large clause weights.
- IND instances: IncWMaxSatz, MSUnCore, and WBO solved all IND instances, whereas other MaxSAT solvers aborted most of them.Among PBO solvers, SAT4J (PB) and BSOLO performed best on the considered benchmark set.
- Detailed comparison: MSUnCore was the best-performing selected solver, followed by WBO and IncWMaxSatz; IncWMaxSatz was more efficient than WBO at smaller run times.The comparison used run-time plots for IncWMaxSatz, MSUnCore, and WBO.
- Encoding choices: The results suggest that encoding cardinality constraints into CNF may outperform native handling of cardinality and pseudo-Boolean constraints for these instance classes.All considered instances could be encoded with cardinality constraints whose polynomial encodings guarantee arc-consistency.
6 Related Work
Related work covers MaxSAT and PBO solvers, their translations, and unsatisfiability-based methods. The paper positions MSUnCore as the first unsatisfiability-based solver for (Partial) Weighted MaxSAT and WBO as a new unified modeling framework.
- MaxSAT and PBO approaches: Prior work surveyed MaxSAT and PBO solvers, translations between the formalisms, and unsatisfiability-based MaxSAT algorithms.The paper uses these surveyed approaches in later sections.
- Paper positioning: The paper identifies MSUnCore as the first algorithm for (Partial) Weighted MaxSAT using unsatisfiable sub-formula identification.The claim is stated as being to the authors' knowledge.
- Paper positioning: The paper presents WBO and its associated algorithm as new contributions within this line of work.The authors describe WBO as a new modeling framework.
- SMT connections: Optimization procedures in SMT also use relaxation variables, similarly to PBO approaches for solving MaxSAT.This connects the paper's optimization setting with related SMT optimization methods.
7 Conclusions and Future Work
The paper introduces WBO as a unified framework for PBO and MaxSAT and extends unsatisfiability-based algorithms to it. Experiments report orders-of-magnitude improvements for weighted MaxSAT and show that a general WBO algorithm can match dedicated algorithms, while future work targets further algorithm extensions.
- Contributions: WBO aggregates and generalizes PBO and MaxSAT, and unsatisfiability-based weighted MaxSAT algorithms can be extended to solve WBO problems.The paper also illustrates extensions of other PBO and MaxSAT algorithms to WBO.
- Empirical results: The new weighted MaxSAT algorithm outperformed existing algorithms by orders of magnitude on a representative benchmark set.The reported experiments also compare native pseudo-Boolean handling with translation to CNF.
- Empirical results: A general WBO algorithm was as efficient as other dedicated algorithms in the reported experiments.This conclusion is based on the representative benchmark instances used in the study.
- Implications and future work: Integrating MaxSAT and PBO into one SAT optimization extension increases the range of problems that can be solved.The framework also supports developing general-purpose algorithms that combine techniques from both domains.
- Implications and future work: Future work includes adapting other algorithms to WBO, including PBO solvers and the existing family of MSU algorithms.