TT-Open-WBO-Inc: An Efficient Anytime MaxSAT Solver
Abstract
We present our anytime MaxSAT solver TT-Open-WBO-Inc, focusing on its evolution since the initial version that won both of the weighted incomplete tracks of MaxSAT Evaluation 2019 (MSE19). The solver’s MSE20 version claimed victory in these tracks at MSE20 and secured second place in both unweighted incomplete tracks. The major innovation in the MSE20 version was the integration of SAT-based local search. The contributions of this paper include: (1) Introducing a previously unpublished variant of the SAT-based local search algorithm Polosat, Polosat-OBV, applied by default already in the MSE20 version, and showing its superiority for weighted solving; (2) Describing and analyzing TT-Open-WBO-Inc’s unweighted component, not studied in previous work; (3) Demonstrating that integrating the local search algorithm SATLike into TT-Open-WBO-Inc as a preprocessor enables it to outperform the winners of MSE20 in all four incomplete tracks.
1.Introduction
MaxSAT is a widely used extension of SAT to optimizing a linear Pseudo–Boolean (PB) function. Given a set of hard propositional clauses H and a target bit-vector (target)
This paper presents the latest version of our anytime MaxSAT solver TT-Open-WBO-Inc. Our solver’s initial release, described in [6], was spawned from the MSE18 version of Open-WBO-Inc [3]. That release won both of the weighted incomplete tracks of MSE19. The major innovations in the next MSE20 version included the integration of the SAT-based local search [8] and the enablement of unweighted solving. The current paper covers:
1) a previously unpublished variant of the SAT-based local search algorithm Polosat [8], Polosat-OBV, applied by default already at MSE20. Section 3 demonstrates Polosat-OBV’s superior performance over Polosat for weighted solving, thus Polosat-OBV contributed to the solver winning both weighted incomplete tracks at MSE20.
2) TT-Open-WBO-Inc’s unweighted component’s architecture, previously undescribed. The solver came in second in both unweighted incomplete tracks at MSE20.
3) showing that by incorporating the local search solver SATLike [2] for preprocessing, TT-Open-WBO-Inc surpasses the winners of MSE20 in all four incomplete tracks.
The baseline algorithm for both weighted and unweighted solving in Open-WBO-Inc, inherited by TT-Open-WBO-Inc, is Linear Search SAT-UNSAT (LSU) [4]. LSU finds the first model
1.1.Weighted Component of TT-Open-WBO-Inc
Table 1 tracks the evolution of the weighted component of TT-Open-WBO-Inc. The baseline algorithm, BMO, is inherited from Open-WBO-Inc [3]. BMO is an incomplete algorithm that approximates weighted solving by clustering the target bits to groups of roughly similar (possibly relaxed) weight and applying LSU over these groups from the highest towards the lowest weights (inspired by Boolean Multilevel Optimization [1]). For MSE19, we incorporated the polarity and variables selection heuristics TORC and TSB, respectively [6,7], to bias the SAT solver towards both the best solution so far and the optimal solution. Specifically, TORC always chooses 0 as the initial polarity for the target bits, whereas, for non-target bits, it picks their value in the best solution so far (if already available). TSB boosts the scores of the target bits at the beginning. For MSE20, we enhanced the weighted component by a new variant of Polosat, Polosat-OBV. Section 2 below reviews Polosat and introduces Polosat-OBV. Finally, for this paper, we also integrated the (classical) local search solver SATLike [2], which we apply for preprocessing similarly to the winner of MSE20 in incomplete unweighted tracks SATLike-20 as follows: obtain a first solution with SAT, improve it for 15 sec. with SATLike and switch to the main SAT-based flow.
1.2.Unweighted Component of TT-Open-WBO-Inc
Consider Table 2, which tracks the evolution of the unweighted component of our solver. Its baseline algorithm is Mrs.Beaver [5], inherited from Open-WBO-Inc [3]. Mrs.Beaver approximates MaxSAT by Optimization Modulo Bit-Vectors (OBV) [9]. OBV is an optimization problem akin to MaxSAT, with the only distinction being that OBV’s objective is to minimize the value of the target T (where T is interpreted as an unsigned number), that is, in OBV, the order of the target bits matters. Mrs.Beaver comprises two stages. The first incomplete stage tries to quickly improve the best known solution by iteratively applying the OBV-BS OBV algorithm. Briefly, OBV-BS works as follows. It goes down the target bits from the MSB towards the LSB, where, for the current bit i, it checks if there is a solution with
As summarized in Table 2, we upgraded the unweighted component for MSE20 as follows. First, we added TORC (omitting TSB due to preliminary experiments showing no benefit in unweighted solving). Second, we enhanced Mrs.Beaver by the following two heuristics from Sect. IV.1 in [7]: Global Stopping Condition (GSC) and Size-based Switching to Complete Part (SSCP). With SSCP, Mrs.Beaver switches from the incomplete to the complete stage whenever the number of clauses expected to be generated by LSU (for blocking all the solutions of weight
Table 2.
MSE | Algorithm | Functionality | Incorporation | Ref. |
– | Polosat | SAT-based local search | Supplant Polosat-OBV | [8] |
SATLike | Classical local search | Preprocess for 15 sec. | [2] | |
2020 | Polosat-OBV | SAT-based local search | Replace SAT queries | New |
GSC & SSCP | Mrs. Beaver heuristics | Modify Mrs. Beaver | [7] | |
TORC | SAT heuristic | Change default heuristic | [7] | |
2018 | Mrs. Beaver | SAT-based MaxSAT flow | Baseline (Open-WBO-Inc) | [5] |
The following Section 2 is about SAT-based local search: it reviews Polosat and introduces Polosat-OBV. Section 3 is dedicated to experimental results. Section 4 concludes our work.
2.SAT-Based Local Search: Polosat and Polosat-OBV
Alg. 1 presents the code of both Polosat [8] and our new Polosat-OBV algorithm.
2.1.Polosat
Consider Alg. 1 in Polosat mode (with lines 8 to 13 disabled). It implements Alg. 2 in [8]. Polosat can be understood as a SAT-based local search algorithm. First, it invokes a SAT solver to get the first model and stashes that model in μ. Then it enters a loop, where each iteration is called an epoch. Each epoch tries to improve the best model so far μ. The algorithm finishes and returns μ, when a certain epoch cannot improve μ anymore.
Each epoch goes over the so-called bad target bits B, where a target bit is considered bad if it has not been assigned 0 in any model from the beginning of the current epoch. The algorithm tries to flip each bad target bit
2.2.Polosat-OBV
The idea behind our new Polosat-OBV algorithm is as follows. Let
Algorithm 1
2.3.Polosat and Polosat-OBV Integration into TT-Open-WBO-Inc
We integrated Alg. 1, which supports both Polosat and Polosat-OBV into TT-Open-WBO-Inc as follows. SAT invocations are replaced by Alg. 1 invocations, where the target bits are sorted by their weight in decreasing order and target bits having the same weight are randomly shuffled. In addition, we apply an adaptive strategy that stops Alg. 1 forever and falls back to SAT whenever the model generation rate of Alg. 1 is slower than n model per second, where
3.Experimental Results
In this section, we study the performance of both weighted and unweighted components of TT-Open-WBO-Inc and compare it to the state-of-the-art solvers SATLike-cw-20 (weighted) and SATLike-c-20 (unweighted) [2]. We ran the following 6 configurations of TT-Open-WBO-Inc for both the weighted and unweighted cases: TT-
We used MSE20 benchmarks. We calculated the score
On weighted instances, our new Polosat-OBV algorithm considerably outperforms Polosat, independently of whether SATLike is used. Moreover, combining SAT-based local search and the classical local search yields excellent results. The resulting solver TT-SL-PolOBV is significantly more efficient than both the version without SATLike (TT-NoSL-PolOBV), which won MSE20, and the version without any SAT-based local search (TT-SL-NoPol).
In a striking difference from the weighted case, in the unweighted scenario, the best-performing version over time utilizes Polosat instead of Polosat-OBV, and the overall impact of Polosat is less significant than in the weighted case. The reason might be related to the similarity of the additional context-query in Polosat-OBV to the SAT queries in the OBV-BS-based underlying Mrs.Beaver algorithm. In a sense, Mrs.Beaver already implements a variant of SAT-based local search with context-queries only. Integrating SATLike yields excellent results similarly to the weighted case. The best resulting solver TT-SL-Polosat outeprforms the winner of MSE20, SATLike-c-20, for every time interval.
Figure 1.
Figure 2.
4.Conclusion
We presented the latest version of our state-of-the-art anytime MaxSAT solver TT-Open-WBO-Inc. Our exposition included: (1) Describing a previously unpublished variant of the SAT-based local search algorithm Polosat, Polosat-OBV, and concluding that Polosat-OBV is superior for weighted solving, while Polosat is better for unwegihted solving. (2) Detailing TT-Open-WBO-Inc’s unweighted component, which has not been examined in prior work; (3) Showing that incorporating the local search solver SATLike [2] for preprocessing allows TT-Open-WBO-Inc to surpass the winners of MSE20 in all four incomplete tracks.
Notes
1 The code of the solvers we have used and instructions on how to reproduce our experiments are available at https://drive.google.com/file/d/1QIx0oyBZOBXtxXqHPubvfZt0XSXkxjcG/view?usp=sharing.
References
[1] | J. Argelich, I. Lynce and J.P. Marques Silva, On solving Boolean multilevel optimization problems, in: IJCAI 2009, pp. 393–398. |
[2] | S. Cai and Z. Lei, Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability, Artif. Intell. 287: ((2020) ), 103354. doi:10.1016/j.artint.2020.103354. |
[3] | S. Joshi, P. Kumar, S. Rao and R. Martins, Open-wbo-inc: Approximation strategies for incomplete weighted maxsat, J. Satisf. Boolean Model. Comput. 11: (1) ((2019) ), 73–97. |
[4] | D. Le Berre and A. Parrain, The sat4j library, release 2.2, JSAT 7: (2–3) ((2010) ), 59–64. |
[5] | A. Nadel, Solving MaxSAT with bit-vector optimization, in: SAT 2018, (2018) , pp. 54–72. |
[6] | A. Nadel, Polarity and variable selection heuristics for SAT-based anytime MaxSAT, J. Satisf. Boolean Model. Comput. 12: ((2020) ), 17–22. |
[7] | A. Nadel, Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization, in: FMCAD 2019, pp. 193–202. |
[8] | A. Nadel, On optimizing a generic function in SAT, in: FMCAD 2020, pp. 205–213. |
[9] | A. Nadel and V. Ryvchin, Bit-vector optimization, in: TACAS 2016, pp. 851–867. |