SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract)

1 Introduction

Discrete decision-making problems crop up in many contexts in the modern world. Such problems can be expressed as constraint satisfaction (or optimisation) problems (CSPs or COPs), then solved using a variety of solver types. An increasingly popular and successful approach to solving CSPs and COPs is to encode them into Boolean formulas and then to apply an off-the-shelf SAT solver. This approach is attractive because of the power of modern conflict-directed clause learning (CDCL) SAT solvers, which incorporate conflict learning, powerful search heuristics, and fast propagation of the Boolean constraints.

Linear equations and inequalities are ubiquitous in constraint problems such as scheduling, routing, resource allocation, and many other hard combinatorial problems. PseudoBoolean (PB) constraints are a particular type of linear constraint of the following form, where q1, . . . , qn and K are integer constants, and x1, . . . , xn are 0/1 variables:

∗This is an extended abstract of the paper [Bofill et al., 2022], that was published in the Artificial Intelligence journal in 2022.

There has been a great deal of work on encoding PB constraints to SAT, some of which is reviewed by Philipp and Steinke [2015]. State-of-the-art encodings are based on Binary Decision Diagrams [E´en and Sorensson, 2006; Ab´ıo et al., 2012], Sequential Weight Counters [H¨olldobler et al., 2012], Generalized Totalizers [Joshi et al., 2015; Zha et al., 2019], and Polynomial Watchdog schemes [Bailleux et al., 2009; Manthey et al., 2014]. At-most-one (AMO) constraints (i.e. constraints of the form ∑mi=1 xi ≤ 1) are also very common, with the most basic being a mutual exclusion between two 0/1 variables.

Combinations of PB and AMO constraints usually appear in settings where one option has to be chosen among a set of incompatible options, and the decision has an associated cost. Bofill, Coll, Suy, and Villaret [Bofill et al., 2017b; Bofill et al., 2020] proposed a SAT encoding based on Multi-valued Decision Diagrams (MDDs) for a conjunction of a PB constraint with a set of AMO constraints over the variables of the PB constraint. Such conjunctions are referred to as PB(AMO) constraints. The AMO constraints (which are encoded separately and may be encoded to SAT using any AMO encoding) allow certain interpretations to be erased from decision diagrams, and to represent the PB constraint as an MDD instead of as a Binary Decision Diagram (BDD). The encoding of the MDD is notably smaller than the encoding of an equivalent BDD, and the solving time is substantially reduced. This technique has been used to provide efficient formulations of particular kinds of scheduling problems [Bofill et al., 2017b; Bofill et al., 2017a]. Also, Ans´otegui et al. [2019] integrated the MDD-based SAT encoding of PB(AMO) constraints into the automatic reformulation pipeline of Savile Row [Nightingale et al., 2017], showing important size and solving time improvements compared to a BDD-based encoding oblivious to the existence of AMO constraints.

This work is an extended abstract of Bofill et al. [2022], whose main contribution is to generalize five state-of-the-art SAT encodings of PB constraints to encode PB(AMO) constraints, as well as the introduction of new optimizations for already existing encodings of PB constraints. In this extended abstract we provide a summary of the main idea behind the generalizations (Section 2), an overview of the new encodings (Sections 3, 4 and 5), and we briefly comment on the results of our experimental evaluation (Section 6).

In this extended abstract we just provide schematic representations of the developed encodings as well as a short description of the encoding idea, so that the reader can visually appreciate the size reductions achieved thanks to using PB(AMO) encodings. The original work contains many other details, including: normalization and reduction techniques for PB(AMO) constraints; detailed explanation of the existing PB encodings and the introduced ones; formal definitions of the clauses introduced by the different encodings; detailed examples for all encodings; proofs of correctness, sizes and propagation properties of all encodings; new heuristics to build unbalanced totalizers that generate smaller formulas; and extensive experiments with two representative SAT solvers on existing and new benchmarks for different problem classses, namely: the Nurse Scheduling problem, the Combinatorial Auctions problem, the Multimode Resource-Constrained Project Scheduling Problem, the Resource-Constrained Project Scheduling Problem with Time-Dependent Resource Capacities and Requests; and the Multi-choice Multidimensional Knapsack Problem.

2 Encoding Technique

There exist a myriad of techniques to encode AMO and PB constraints to SAT. Therefore, the straightforward approach for a problem containing both kinds of constraints is to encode each of them separately with some existing technique, and join the resulting sets of clauses. However, when the variables of a PB constraint also occur in AMO constraints, we can do much better. As a motivating example, consider the PB constraint:

Also, suppose there are two AMO constraints: x1+x2+x3≤1 and x4+x5+x6≤1. Encoding the PB constraint alone would require several clauses and (depending on the chosen encoding) multiple additional variables. For example, the Generalized Totalizer encoding [Joshi et al., 2015] has 23 additional variables and 56 clauses. However, the two AMO constraints rule out most of the values that the sum (2x1+· · ·+4x6)

could take, and almost all such values that break the PB constraint. Encoding the PB constraint together with the two AMO constraints requires just one clause to prevent x3 and x6 being assigned true together. This simple observation underpins all the PB(AMO) encodings presented in this paper.

In our encodings, we consider PB constraints such that all their variables also belong to some AMO constraint. Notice that this is not a limitation in the sense that any single variable x can constitute itself an AMO constraint x ≤ 1 if no other AMO constraint contains it. Moreover, we require the AMO constraints to be disjoint. Again, this is not a limitation, since we can always remove variables from AMO constraints to achieve this property, e.g. if we have the constraint x1+x2+x3≤1, implicitly we also have the constraint x1+x2≤1. We refer to this kind of conjunction between one PB constraint and a set of AMO constraints as a PB(AMO) constraint.

The encoding technique we employ for PB(AMO) constraints works as follows. First, we will encode all AMO constraints with some existing technique, thus obtaining a set of clauses F1. Then, instead of constructing a full encoding of the PB constraint, we construct a simplified version assuming that the AMO constraints will hold, obtaining a set of clauses F2. The resulting encoding of the PB(AMO) constraint is F1 ∪F2. In order to take into account the AMO constraints in the second step, we consider the PB constraint and a partition of its variables. In particular, the variables of each part corresponds to the variables of a different AMO constraint. For instance, in the motivating example given before, we consider the tuple:

One encoding of the example would be F1 = {(x1 ∨ x2), (x1 ∨ x3), (x2 ∨ x3), (x4 ∨ x5), (x4 ∨ x6), (x5 ∨ x6)}, and F2 = {(x3 ∨ x6)}.

The generation of F1 can be easily achieved with any existing encoding technique for AMO constraints. In this work we present many encoding techniques for F2, taking as input the PB constraint and variable partition.

3 Sequential Weight Counter Encoding

The Sequential Weight Counter encoding for PB constraints was defined in [H¨olldobler et al., 2012], and is illustrated by Figure 1 (left). The resulting CNF formula simulates a circuit that sequentially sums the coefficients of the variables assigned 1. For each variable, we include a component (counter) that increases (if needed) the accumulated sum value. Finally, the clauses of the encoding also require that the sum never exceeds the maximum allowed by the PB constraint.

Taking into account that some subsets of variables satisfy an AMO constraint, we can reduce the number of counters. In particular, all the variables of a same part of the partition (AMO constraint) share the same counter. As illustrated by Figure 1 (right), this effectively decreases the number of counters, and therefore the number of output pins (auxiliary variables) and the number of clauses.

4 Totalizer-Based Encodings

A totalizer is a binary tree where the leaf nodes represent items to be summed, and each non-leaf node represents the sum of its two children. An encoding of PB constraints based on totalizers was presented by Joshi et al. [2015] and named Generalized Totalizer (GT). In GT, each leaf node is attached to a single PB term qixi, and takes the value qi when xi is true and 0 otherwise. An example of a totalizer representing a PB constraint can be seen in Figure 2 (left). The SAT encoding consists of a CNF formula simulating the totalizer as well as a clause forbidding that the maximum allowed sum is exceeded at the root node. Note that each node of a totalizer represents an integer value. In the GT encoding, these values are (roughly) represented as an order encoding, i.e., for each value v ∈ 0, . . . , k, that a node O can take, we introduce the variable o≥v. The encoding is optimized by only introducing auxiliary variables o≥v for values v that are reachable by adding the two children.

Zha et al. [2019] presented an alternative totalizer-based encoding for PB constraints, named n-level MTO (Modulo Totalizer). In the MTO, the value of the nodes is represented with a decomposition into multiple digits in a mixed radix base. For instance, in a decimal decomposition, we would introduce variables representing the value of the units, variables for the tens, the hundreds, the thousands, etc. This typically results in much smaller formulas but with weaker propagation properties.

In our work we present generalizations of both GT and MTO to encode PB(AMO) constraints. The overall idea of the generalization is the same in both cases and illustrated in Figure 2 (right). Here, instead of associating only one variable to a leaf node, we associate all the variables of an AMO. However, the way of achieving this association is different for GT and for MTO (more details can be found in the full paper). By grouping the variables of the AMO constraints, we can reduce the number of leaves of the totalizer which in turn will reduce the number of clauses and auxiliary variables of the encoding.

Another contribution of our work is a new totalizer-based encoding, which is novel not only for the PB(AMO) case but also for the classical PB setting. We call this encoding the Reduced Generalized Totalizer (RGT). The starting point of RGT is the tree structure of the GT encoding. Once the tree is constructed, it applies a reduction algorithm in order to obtain a more compact representation that replaces individual numeric values with intervals. In some cases, RGT will detect that terms in the PB constraint are redundant. When this occurs the redundant terms are removed and the entire encoding process is repeated (until a fixpoint is reached). RGT is frequently substantially smaller than GT and this translates to improved solver efficiency.

5 Watchdog-Based Encodings

Two different PB encodings were presented in [Bailleux et al., 2009], namely the Global Polynomial Watchdog (GPW) and the Local Polynomial Watchdog (LPW). Both of them use as a basis a so-called polynomial watchdog circuit, represented in Figure 3 (left). GPW uses just one polynomial watchdog, while LPW introduces one polynomial watchdog for each variable, and the practical difference is that the former results in smaller formulas but with weaker propagation properties. This kind of circuit decomposes the coefficients of the variables in a binary representation. The variables of every bit are added with sorter circuits, and the different bits are later added in merger circuits. Whenever the maximum value of the PB is surpassed, the so-called watchdog pin (variable) w is set to true.

The basic idea of our PB(AMO) generalization, illustrated in Figure 3 (right), is to represent the j-th bit of all variables of the i-th AMO with a single auxiliary variable yi,j . This can reduce the number of inputs of the sorters, and by extension reduce the number of variables of clauses not only to encode the sorters but also the mergers, as can be appreciated with the decrease of pins in Figure 3 (right).

Moreover, in the original work we present many formula reduction techniques for watchdog-based encodings, especially for LPW, based on reusing pins and components of the circuits. These size reductions are especially suitable in the PB(AMO) case, where the assumption of AMO constraints allows for extra circuit reuses.

6 Results

As proved in the original work, the newly introduced encodings for PB(AMO) constraints maintain the same propagation strength by unit-propagation that their PB counterparts have. We also achieve theoretical size reduction of the encodings, both in terms of number of auxiliary variables and number of clauses. This is certified by our experimental section, where we can identify size reductions of up to three orders of magnitude. This reduction in size has a clear impact on the solving times, which are drastically reduced with the PB(AMO) approach, based on experiments conducted with two recent CDCL SAT solvers. Compared to their PB counterparts, PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases. Similarly, the new totalizer-based encoding and the presented totalizerbuilding heuristic also generate smaller encodings and improve the solving times.

In Table 1 we show a few selected experimental results from the full paper, with five encodings chosen from the eight encodings in the full paper, with only one problem class, and with only one SAT solver. The selected results show very clear benefits from using PB(AMO) encodings on that problem class, with a very substantial reduction in the number of time-out instances.

We also show empirically the usefulness of having distinct encodings with different properties, usually with trade-offs between number of variables, number of clauses and propagation strength, since the best choice depends on the tackled problem class.

Acknowledgments

This work has been partially supported by Grants PID2019-111544GB-C21, TED2021-129319B-I00 and PID2021-122274OB-I00 funded by MCIN/AEI /10.13039/501100011033 and by ERDF A way of making Europe, and by Grant EP/R513386/1 from the UK Engineering and Physical Sciences Research Council.