Optimizing SAT Encodings for Arithmetic Constraints

Abstract

The log encoding has been perceived to be unsuited to arithmetic constraints due to its hindrance to propagation. The surprising performance of PicatSAT, which is a pure eager SAT compiler based on the log encoding, in the MiniZinc Challenge 2016 has revived interest in the log encoding. This paper details the optimizations used in PicatSAT for encoding arithmetic constraints. PicatSAT adopts some well-known optimizations from CP systems, language compilers, and hardware design systems for encoding constraints into compact and efficient SAT code. PicatSAT is also empowered by a novel optimization, called equivalence reasoning, for arithmetic constraints, which leads to reduction of code size and execution time. In a nutshell, this paper demonstrates that the optimized log encoding is competitive for encoding arithmetic constraints.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The drastic enhancement of SAT solvers’ performance has made SAT a viable backbone for general CSP (Constraint Satisfaction Problem) solvers [8, 21, 30, 33, 34]. Many real-world combinatorial problems involve arithmetic constraints, and it remains a challenge to efficiently encode arithmetic constraints into SAT. The sparse encoding [20, 36] and order encoding [13, 25, 34] can easily blow up the code size, and the log encoding [18, 22] is perceived to be a poor choice, despite its compactness, due to its failure to maintain arc consistency, even for binary constraints. This dilemma of the eager approach has led to the emergence of the lazy approach, as represented by SMT solvers that use integer arithmetic as a theory [6, 14, 26] and the lazy clause generation (LCG) solver that combines SAT and constraint propagation [17, 29]. Both the eager and lazy approaches have strengths and weaknesses [27]. For problems that require frequent checking of arithmetic constraints the lazy approach may not be competitive due to the overhead, even when checking is done incrementally and in a priori manner. From an engineering perspective, the eager approach also has its merit, just like the separation of computer hardware and language compilers is beneficial.

The surprising performance of the PicatSAT compiler in the MiniZinc Challenge 2016 is thought-provoking.¹ PicatSAT is a pure SAT compiler that translates CSPs into log-encoded SAT code. PicatSAT adopts the sign-and-magnitude log encoding for domain variables. For a domain with the maximum absolute value n, it uses $log_2(n)$ Boolean variables to encode the domain. If the domain contains both negative and positive values, then another Boolean variable is employed to encode the sign. Each combination of values of the Boolean variables represents a valuation for the domain variable. The addition constraint is encoded as logic adders, and the multiplication constraint is encoded as logic adders using the shift-and-add algorithm.

PicatSAT adopts some well-known optimizations from CP systems, language compilers, and hardware design systems for encoding constraints into compact and efficient SAT code: it preprocesses constraints before compilation in order to remove no-good values from the domains of variables whenever possible; it eliminates common subexpressions so that no primitive constraint is duplicated; it uses a logic optimizer to generate optimized code for adders. These optimizations significantly improve the quality of the generated code.

This paper proposes a new optimization, named equivalence reasoning, for log-encoded arithmetic constraints. Equivalence reasoning identifies information about if a Boolean variable is 0 or 1, if a Boolean variable is equivalent to another Boolean variable, or if a Boolean variable is the negation of another Boolean variable. This optimization can reduce both the number of Boolean variables and the number of clauses in the CNF code.

The experimental results show that equivalence reasoning reduces code sizes, and for some benchmarks, significantly reduces the solving time. The MiniZinc Challenge 2016 results show that PicatSAT outperformed some of the fastest CP solvers in the competition. Our new comparisons of PicatSAT with fzn2smt, an SMT-based CSP solver, and Chuffed, a cutting-edge LCG solver, also reveal the competitiveness of PicatSAT.

2 The PicatSAT Compiler

PicatSAT is offered in Picat as a module named sat. In addition to the sat module, Picat offers two other solver modules, named cp and mip, respectively. All these three modules implement the same set of basic linear constraints over integer domains and Boolean constraints. The cp and sat modules also implement non-linear and global constraints, and the mip module also supports real-domain variables. The common interface that Picat provides for the solver modules allows seamless switching from one solver to another.

In order to give the reader a complete picture of the PicatSAT compiler, we give in this section an overview of the compiler, including the adopted optimizations. A description of a preliminary version of PicatSAT with no optimizations is given in [38].

2.1 Preprocessing and Decomposition

In general, a constraint model consists of a set of decision variables, each of which has a specified domain, and a set of constraints, each of which restricts the possible combinations of values of the involved decision variables. A constraint program normally poses a problem in three steps: (1) generate variables; (2) generate constraints over the variables; and (3) call solve to invoke the solver in order to find a valuation for the variables that satisfies the constraints and possibly optimizes an objective function.

PicatSAT preprocesses the accumulated constraints when the solve predicate is called. For binary equality constraints, PicatSAT excludes no-good values from the domains to achieve arc consistency, unless the domains are too big.² For instance, for the constraint $X = 9*B+1$, where B is a Boolean variable that has the domain 0..1, PicatSAT narrows X’s domain to $\{1,10\}$. For other types of constraints, including binary equality constraints that involve large-domain variables, PicatSAT narrows the bounds of domains to archieve interval consistency.

PicatSAT decomposes arithmetic constraints into basic constraints, including primitive, reified, and implication constraints. A primitive constraint is one of the following: $\Sigma _{i}^nB_i\ r\ c$ (r is $=$, $\ge$, or $\le$, and c is 1 or 2),³ $X\ r\ Y$ (r is $=$, $\ne$, >, $\ge$, <, or $\le$), $X+Y = Z$, and $X\times Y = Z$, where $B_i$ is a Boolean variable, and X, Y, and Z are integers or integer domain variables. A reified constraint, after decomposition, takes the form $B \Leftrightarrow C$, and an implication constraint has the form $B \Rightarrow C$, where B is a Boolean variable, and C is a primitive constraint.

For a linear constraint, PicatSAT sorts the terms by the variables. This ordering facilitates merging terms of the same variables, but is hardly optimal for generating efficient SAT code. PicatSAT breaks down Pseudo-Boolean (PB) constraints, including cardinality constraints, in the same way as other linear constraints, unless they are cardinality constraints of the form $\Sigma _{i}^nB_i\ r\ c$ (c =1 or 2). For example, the cardinality constraint $U+V+W+X \le 3$, where all the variables are Boolean, is split into the following primitive constraints:

This method of decomposing PB constraints is simple, and generates compact code. For a cardinality constraint that has n variables, this method introduces O(n) auxiliary integer-domain variables, which require a total number of $O(n\times log_2(n))$ Boolean variables to encode.⁴

During decomposition, PicatSAT introduces auxiliary variables to combine terms in the same way as language compilers break expressions into triplets. PicatSAT makes efforts not to create variables with both positive and negative values in their domains, if possible, because such a domain requires a sign bit and cannot be encoded compactly. For example, for the constraint $U-V+W-X \le 3$, PicatSAT merges U with W, and V with X so that no auxiliary variables have negative values in their domains if the domains of the original variables do not contain negative values.

PicatSAT eliminates common subexpressions in constraints. Whenever PicatSAT introduces an auxiliary variable for a primitive constraint, it tables the constraint. When the same primitive constraint is encountered again, PicatSAT reuses the auxiliary variable, rather than introducing a new variable for the constraint. For example, when a reification constraint $B \Leftrightarrow C$ is generated, PicatSAT tables it and reuses the variable B, rather than introducing a new variable for the primitive constraint C, when C is encountered again in another constraint. The algorithm used in PicatSAT for identifying common subexpressions is not as sophisticated as those used in [4, 28]. It incurs little overhead on compilation, but fails to eliminate common subexpressions in many cases.

2.2 The Sign-and-Magnitude Log Encoding

PicatSAT employs the log-encoding for domain variables. For a domain variable, $\lceil log_2(n)\rceil$ Boolean variables are used, where n is the maximum absolute value in the domain. If the domain contains both negative and positive values, then another Boolean variable is employed to represent the sign. In this paper, for a log-encoded domain variable X, X.s denotes the sign, X.m denotes the magnitude, which is a vector of Boolean variables $<X_{n-1}X_{n-2}\ldots X_{1}X_0>$.

This sign-and-magnitude encoding requires a clause to disallow negative zero if the domain contains values of both signs. Each combination of values of the Boolean variables represents a valuation for the domain variable: $X_{n-1}\times 2^{n-1}+X_{n-2}\times 2^{n-2}+\ldots +X_{1}\times 2+X_0$. If there are holes in the domain, then not-equal constraints are generated to disallow assigning those hole values to the variable. Also, inequality constraints ($\ge$ and $\le$) are generated to prohibit assigning out-of-bounds values to the variable if either bound is not $2^k-1$ for some k.

For small-domain variables, PicatSAT calls the logic optimizer, Espresso [9], to generate an optimal or near-optimal CNF formula. For example, for the domain constraint $X{:}{:} \, [-2,-1,2,1]$, one Boolean variable, S, is utilized to encode the sign, and two variables, $X_1$ and $X_0$, are employed to encode the magnitude. A naive encoding with conflict clauses [18] for the domain requires four clauses:

These clauses correspond to four no-good values: -3, -0, 0, and 3, where -0 denotes the negative 0. Espresso only returns two clauses for the domain:

Note that the sign variable is optimized away.

2.3 Encoding Basic Constraints

The encodings for the addition and multiplication constraints will be described in later sections. This subsection briefly describes the Booleanization of other basic constraints.

The at-least-one constraint $\Sigma _{i}^{n}B_i \ge 1$ is encoded into one CNF clause:

The at-least-two constraint $\Sigma _{i}^{n}B_i \ge 2$ is converted into n at-least-one constraints: for each $n-1$ variables, the sum of the variables is at least one. The at-most-one constraint $\Sigma _{i}B_i \le 1$ is encoded into CNF by using the two-product algorithm [12]. The at-most-two constraint is converted into n at-most-one constraints. The exactly-one constraint $\Sigma _{i}^{n}B_i = 1$ is converted into a conjunction of an at-least-one constraint and an at-most-one constraint. The exactly-two constraint is compiled similarly.

A recursive algorithm is utilized to compile binary primitive constraints. For example, consider $X \ge Y$. This constraint is translated to the following:

PicatSAT simplifies the formula if the variables’ signs are known at compile time. Let X.m = ${<}X_{n-1}X_{n-2}\ldots X_{1}X_0{>}$, Y.m = ${<}Y_{n-1}Y_{n-2}\ldots Y_{1}Y_0{>}$.⁵ PicatSAT introduces auxiliary variables $T_0$, $T_1$, $\ldots$, $T_{n-1}$ for comparing the bits:

PicatSAT then encodes the constraint X.m $\ge$ Y.m as $T_{n-1}$. When either X or Y is a constant, PicatSAT compiles the constraint without introducing any auxiliary variables.⁶

The reified constraint $B \Leftrightarrow C$ is equivalent to $B \Rightarrow C$ and $\lnot B \Rightarrow \lnot C$, where $\lnot C$ is the negation of C. Let $C_1\ \wedge \ \ldots \ \wedge \ C_n$ be the CNF formula of C after Booleanization. Then $B \Rightarrow C$ is encoded into $C_1'\ \wedge \ \ldots \ \wedge \ C_n'$, where $C_i'$ = $(C_i\ \vee \ \lnot B)$ for $i=1,...,n$.

3 Equivalence Reasoning

Equivalence reasoning is an optimization that reasons about a possible value for a Boolean variable or the relationship between two Boolean variables. This reasoning exploits the properties of constraints. For example, consider the domain constraint $X \, {:}{:} \, [2,6]$. The magnitude of X is encoded with three Boolean variables $X.\mathtt{m} = <X_2,X_1,X_0>$. PicatSAT infers $X_1$ = 1 and $X_0$ = 0 from the fact that the binary representations of both 2 and 6 end with 10. With this reasoning, PicatSAT does not generate a single clause for this domain.

The following gives several constraints on which PicatSAT performs equivalence reasoning:

Note that the constraint X.m = Y.m is enforced by unifying the corresponding Boolean variables of X and Y at compile time. Equivalence reasoning considerably eases encoding for some of the constraints. For example, the following clause encodes the constraint X = $-$ $Y$, regardless of the sizes of the domains:⁷

and no clause is needed to encode the constraint X = abs(Y).

Equivalence reasoning can be applied to those addition and multiplication constraints that involve constants. We call this kind of equivalence reasoning constant propagation. The remaining of this section gives the propagation rules. In order to make the description self-contained, we include the encoding algorithms for addition and multiplication constraints described in [38].

3.1 Constant Propagation for $X+Y = Z$

For the constraint $X+Y = Z$, if either X or Y has values of mixed signs in its domain, then PicatSAT generates implication constraints to handle different sign combinations [38]. In the following we assume that both operands X and Y are non-negative (i.e., X .s = 0 and Y .s = 0), so the constraint $X+Y = Z$ can be rewritten into the unsigned addition X .m+ Y .m = Z.m.

Let X.m = $X_{n-1}\ldots X_1X_0$, Y.m = $Y_{n-1}\ldots Y_1Y_0$, and Z.m = $Z_{n}\ldots Z_1Z_0$. The unsigned addition can be Booleanized by using logic adders as follows:

A half-adder is employed for $X_0+Y_0 = C_1Z_0$, where $C_1$ is the carry-out. For each other position i ($0 < i \le n-1$), a full adder is employed for $X_i+Y_i+C_i = C_{i+1}Z_i$. The top-most bit of Z, $Z_{n}$, is equal to $C_n$. This encoding corresponds to the ripple-carry adder used in computer architectures.

The full adder $X_i+Y_i+C_{in} = C_{out}Z_i$ is encoded with the following 10 CNF clauses when all the operands are variables:

If any of the operands is a constant, then the code can be simplified. For example, if $C_{in}$ is 0, then the full adder becomes a half adder, which can be encoded with 7 CNF clauses.

For the half adder $X_i+Y_i = C_{out}Z_i$, if any of the operands is a constant, PicatSAT infers that the other two variables are equal or one variable is the negation of the other. PicatSAT performs the following inferences when X or Z is a constant:

 

Rule-1::

$X_i = 0 \Rightarrow C_{out} = 0 \wedge Z_i = Y_i.$

Rule-2::

$X_i = 1 \Rightarrow C_{out} = Y_i \wedge Z_i = \lnot Y_i.$

Rule-3::

$Z_i = 0 \Rightarrow C_{out} = X_i \wedge X_i = Y_i$

Rule-4::

$Z_i = 1 \Rightarrow C_{out} = 0 \wedge X_i = \lnot Y_i.$

Similar inference rules apply when $Y_i$ is a constant.

For example, consider the addition:

PicatSAT infers the following equivalences:

Consider, as another example, the addition:

PicatSAT infers the following equivalences:

The last two equivalences, $X_2 = 1$ and $Y_2 = 1$, are obtained by Rule-3 and the fact that $Z_3 = 1$.

When PicatSAT infers an equivalence between two variables or between one variable and another variable’s negation, PicatSAT only uses one variable in the CNF code for the two variables, and eliminates the two CNF clauses for the equivalence.

4 Constant Propagation for $X\times Y = Z$

PicatSAT adopts the shift-and-add algorithm for multiplication. Let X.m be $X_{n-1}\ldots X_1 X_0$. The shift-and-add algorithm generates the following conditional constraints for $X\times Y = Z$.

The operation ($Y<< i$) shifts the binary string of Y to left by i positions. Let the length of the binary string of Y be u. The length of $S_0$ is u, that of $S_1$ is $u+1$, and so on. So the total number of auxiliary Boolean variables that are created to hold the sums is $\Sigma _{i=u}^{(n+u-2)}i$ plus the number of auxiliary variables used for carries in the additions. Note that because $S_{n-1}$ is the same as Z, $S_{n-1}$ is never created.

If either X or Y is a constant, the basic algorithm can be improved to reduce the number of auxiliary variables. In the following of this subsection, we assume that X is a constant.

In the conditional constraints:

If $X_i$ is 0, then $S_i$ is the same as $S_{i-1}$, and the variables in $S_{i-1}$ can be reused for $S_i$. If $X_i$ is 1, then the lowest i bits of $S_i$ are the same as the lowest i bits of $S_{i-1}$, and these i variables can be copied from $S_{i-1}$ to $S_i$. The following two rules perform these propagation:

 

Rule 5::

$X_i = 0 \Rightarrow$ copy all of the bits of $S_{i-1}$ into $S_{i}$.

Rule 6::

$X_i = 1 \Rightarrow$ copy the lowest i bits of $S_{i-1}$ into $S_{i}$.

Let $X_i$ be the lowest bit of X that is 1, meaning that $X_j = 0$ for $j \in 0..i-1$. Then $Z_i$ is the same as $Y_0$, the lowest bit of Y, and $Z_k = 0$ for $k \in 0..i-1$. Here is the rule that performs this propagation:

 

Rule 7::

$X.m =$ $X_{n-1}\ldots X_i0\ldots 0$ $\,\wedge X_i = 1\ \Rightarrow$

$Z_i = Y_0 \wedge Z_k = 0$ for $k \in 0..(i-1)$.

In particular, if X is a power of 2, then Z is the result of shifting Y to left by $n-1$ positions, and no auxiliary variables are needed.

The number of additions performed by the shift-and-add algorithm is the number of 1 s in the binary string of X. If X is a constant that is not a power of 2 but is close to a power of 2, then PicatSAT converts the multiplication into an addition. The following rules perform this optimization:

 

Rule-8::

$X = 2^K -1\ \Rightarrow$

rewrite $X\times Y = Z$ into $2^K\times Y = Z+Y$.

Rule-9::

$X = 2^K -2\ \Rightarrow$

rewrite $X\times Y = Z$ into $2^K\times Y = Z+2\times Y$.

For example, PicatSAT converts the constraint $7\times X = Z$ to $8\times X = Z + X$, which requires one addition while the original constraint requires three additions.

5 Experimental Results

PicatSAT, which is implemented in Picat, has about 8,000 lines of code, excluding comments. PicatSAT connects to Lingeling SAT solver (version 587f) through a C interface.

We have done two experiments in order to evaluate the compiler using Picat version 2.1.⁸ In the first experiment, we ran PicatSAT on several benchmark problems that involve arithmetic constraints, and measured the code size and the execution time of each of the benchmarks. These results show how effective equivalence reasoning is on reducing the code size and the execution time.

In the second experiment, which was conducted on Linux Ubuntu 14.04LTS with an Intel i7-5820K 3.30 GHz CPU and 32 GHz RAM, we compared PicatSAT with Chuffed⁹ and fzn2smt version 2.0.02.¹⁰ Chuffed is a cutting-edge LCG solver. The fzn2smt solver, which took the second place in MiniZinc Challenge 2012, translates FlatZinc¹¹ into SMT that is solved by Yices¹².

This section does not include comparisons of PicatSAT with many other state-of-the-art CSP solvers. In the free search category of the MiniZinc Challenge 2016, an old version of PicatSAT outperformed some of the fastest CSP solvers, and was only second to HaifaCSP¹³ by a small margin.

Table 1. Evaluation of effectiveness of equivalence reasoning (code size)

Table 1 evaluates how effective equivalence reasoning is on reducing the code size (#vars, the number of variables, and #cls, the number of clauses). The first three benchmarks are well known puzzles in the CP community. The next three are instances of the magic square problem for the grid sizes of $7\times 7$, $8\times 8$, and $9\times 9$. The remaining 5 benchmarks are integer programming benchmarks taken from [30].¹⁴ The column PicatSAT $^\mathsf{nor}$ shows the results obtained with the equivalence reasoning optimization disabled, and the column PicatSAT shows the results obtained when the optimization was enabled.

As can be seen, the optimization led to certain amounts of reduction in the code size for each of the benchmarks. For crypta, the reduction in code size is most significant; the number of variables is reduced to 54%, and the number of clauses is reduced to 75%. For magic_square, whose code size is dominated by an all-different constraint, the reduction in code size is only 1%.

Table 2 evaluates how effective equivalence reasoning is on reducing the compile time (comp) and the solving time (solve). The solving time of the CNF code was measured using Lingeling version 587f on a Cygwin notebook computer with 2.60 GHz Intel i7 and 64 GB RAM. Interestingly, while the code reduction for magic_square is the least significant, the speedups are the most significant. Overall, the optimization reduces both the compile time and the solving time, and the results show that the equivalence reasoning optimization is worthwhile to incorporate.

Table 2. Evaluation of effectiveness of equivalence reasoning (time, seconds)

Table 3 compares PicatSAT with fzn2smt and Chuffed on the instances used in the MiniZinc Challenge 2012.¹⁵ All of the instances were translated from MiniZinc into FlatZinc using each individual solver’s global constraints.¹⁶ The time limit was set to 15 min per instance, which limits the total of the conversion time and the solving time. For each benchmark, the number in the parentheses is the total number of instances, and the number in each column indicates the number of completely solved instances by the solver. For optimization problems, an instance is considered solved if an optimal solution was given and its optimality was proven. PicatSAT solved 77 instances, while fzn2smt solved 52, and Chuffed solved 67 instances. This experiment demonstrates the competitiveness of PicatSAT in comparison with two lazy-approach-based solvers. When equivalence reasoning was disabled, PicatSAT solved 75 instances. This result also shows the worthiness of the optimization.

Table 3. A comparison of three CSP solvers (solved instances)

6 Related Work

A wide variety of problems have been encoded into SAT and solved by SAT solvers. SAT is also the backbone of many logic language systems, such as formal methods [23], answer set programming [10, 19], and NP-SPEC [11]. PicatSAT is a compiler that translates high-level constraints into SAT. Other SAT compilers include BEE [25], FznTini [21], meSAT [33], and Sugar [34]. PicatSAT, like FznTini, adopts the log encoding, while the other compilers are based on the order encoding.

Despite the compactness of the log encoding, it has received little attention for CSP solving, probably because of its weak propagation strength and its requirement of engineering efforts. FznTini was the only known log-encoding based CSP solver before PicatSAT. FznTini employs the 2’s complement encoding for domain variables, while PicatSAT uses the sign-and-magnitude encoding. FznTini demonstrated the promise of the log encoding, but it lacks optimizations, and is not considered competitive with recent CP solvers [30].

The perception that eager SAT-encoding approaches are not suited to arithmetic constraints has motivated the development of lazy approaches such as SMT [6, 27] and lazy clause generation [17, 29] that integrates CP and SAT solving techniques. Recent MiniZinc competitions have been dominated by LCG solvers; the HaifaCSP solver [35] also performs learning during search.

Encodings, such as BDDs [1, 7] and sorting networks [16], have been proposed for special form of arithmetic constraints, such as Boolean cardinality constraints and Pseudo-Boolean (PB) constraints. Linear arithmetic constraints can be compiled into SAT through PB constraints [2]. This encoding through PB constraints is less compact than the adder-based log encoding, but has stronger propagation power. The hybrid encoding that integrates order and log encodings [32] compiles linear constraints that involve large-domain variables into SAT through PB constraints.

The idea of identifying equivalences and exploiting them to reduce code sizes has been explored in both SAT compilation and SAT solving. The BEE compiler [25] performs equi-propagation, which takes advantage of the properties of the order-encoding to infer equivalences. Although equivalences could be detected to some extent by SAT solvers, it is always beneficial to do the reasoning at compile time, because SAT solvers are unaware of the meaning of the original constraints, and it is expensive to detect equivalences at preprocessing time [15] or reason about them at solving time [24].

PicatSAT embodies optimizations used in CP systems for processing constraints [31], in language compilers for eliminating sub-expressions [3], and in hardware design systems for optimizing logic circuits [9]. The equivalence reasoning optimization, which is specific to the log encoding, has not been implemented in any other SAT compilers.

7 Conclusion

In this paper we have presented the PicatSAT compiler and its optimizations. PicatSAT employs the log encoding, which has received little attention by SAT-based CSP solvers for its lack of propagation strength. PicatSAT adopts optimizations from CP systems (preprocessing constraints to narrow the domains of variables), language compilers (decomposing constraints into basic ones and eliminating common subexpressions), and hardware design systems (using a logic optimizer to optimize codes for adders and other basic constraints). Furthermore, PicatSAT reasons about equivalences in arithmetic constraints, and exploit them to eliminate variables and clauses. With these optimizations, PicatSAT is able to generate more compact and faster code for arithmetic constraints.

This work has shed a light on the debate between the eager and lazy approaches to constraint solving with SAT. The failed attempts to find efficient encodings for arithmetic constraints have motivated the development of the lazy approaches. This paper has shown that the eager approach based on the optimized log encoding is not as bad for arithmetic constraints as it was perceived before. A comparison with an SMT-based CSP solver and a LCG solver shows the competitiveness of PicatSAT.

In addition to the optimizations, including the novel equivalence reasoning optimization, and the engineering effort, the success of PicatSAT is also attributed to Picat, the implementation language. The log encoding is arguably more difficult to implement than the sparse and order encodings. Picat’s features, such as attributed variables, unification, pattern-matching rules, and loops, are all put into good use in the implementation. There are hundreds of optimization rules, and they can be described easily as pattern-matching rules in Picat. Logic programming has been proven to be suitable for language processing in general, and for compiler writing in particular; PicatSAT has provided another testament.

The success of PicatSAT does not in any way undermine the lazy approaches: there are certainly many problems for which the lazy approaches prevail, and many theories incorporated in SMT solvers do not yet have efficient SAT encodings. A comprehensive comparison of eager encoding and lazy approaches is on the stack for future work.

PicatSAT still has plenty of room for improvement, especially concerning global constraints and special constraints. One direction for future work is to carry out these improvements.

The optimizations reported in this paper could be only the tip of the iceberg. Numerous algorithms and optimizations have been proposed for hardware design systems, such as multi-bit and multi-operand adders and multipliers. When multiple bits are considered at once, there will be more reasoning opportunities opening up. Another direction for future work is to investigate these algorithms for SAT encodings.