TT-Open-WBO-Inc: An Efficient Anytime MaxSAT Solver

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 ti=0 using a SAT query (OBV-BS inside Mrs.Beaver limits every SAT query by a 1000 conflict threshold). If no solution is found, ti is fixed to 1. Otherwise, ti and any subsequent satisfied bits ti+1…ti+l are fixed to 0 and the algorithm moves on to testing bit number i+l+1. For improving the odds of finding a good unordered solution with OBV-BS’s ordered approximation, Mrs.Beaver shuffles or reverses the target bits provided to OBV-BS in every iteration; some iterations also push any 0-valued bits towards the MSB after a new model is found [5]. The second complete stage of Mrs.Beaver falls back to LSU.

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 ⩾Ψ(μ1)) is not greater than 106; otherwise, Mrs.Beaver never switches. GSC halts any OBV-BS iteration at the incomplete stage and proceeds to the next one once (and if) the number of target bits fixed to 1 by OBV-BS matches that of the best MaxSAT solution so far (so, no improvement is possible). Third, we incorporated Polosat-OBV. For this paper, we integrated SATLike [2] similarly to the weighted component, and, based on our results in Section 3, reverted from Polosat-OBV to Polosat [8] for unweighted solving.

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.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 ti by sending the SAT solver a flip-query with ¬ti as an assumption. Note that if the flip-query finds any model, it must be different from every other model encountered during the current epoch, since the current bad target bit is enforced to 0. If a model better than μ is found, μ is updated. The set of the bad target bits B is refined, whenever any new model is found.

2.2.Polosat-OBV

The idea behind our new Polosat-OBV algorithm is as follows. Let ti be the current bad target bit, encountered by Polosat. We are interested to make an additional SAT query, called the context-query, prior to the flip-query. For the context-query, the SAT solver is provided with the assumption ¬ti (as in Polosat) along with a set of assumptions assigning the target bit variables tj:1⩽j<i their polarity in μ. The context-query looks for a new model in a more restricted context, induced by the value in μ of the current target prefix. It is expected to come back faster than the flip-query, because of the additional assumptions. If the context-query succeeds to improve the best model, we skip the flip-query for the current bad target bit. Otherwise, the flip-query is applied as usual.

Algorithm 1

Polosat-OBV or Polosat

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 n=1 for the weighted component and n=2 for the unweighted one. We use conflict threshold of 1000 for every SAT query. Furthermore, the weighted component also uses the mutation combination strategy (see Section 3.B in [8]), which tries to combine solutions to create new ones, although mutation combination’s impact is marginal [8].