Automatic Generation of Propagation Complete SAT Encodings

Abstract

Almost all applications of SAT solvers generate Boolean formulae from higher level expression graphs by encoding the semantics of each operation or relation into propositional logic. All non-trivial relations have many different possible encodings and the encoding used can have a major effect on the performance of the system. This paper gives an abstract satisfaction based formalisation of one aspect of encoding quality, the propagation strength, and shows that propagation complete SAT encodings can be modelled by our formalism and automatically computed for key operations. This allows a more rigorous approach to designing encodings as well as improved performance.

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

Almost all industrial applications of SAT solvers translate from a higher level language into propositional logic. Many of these translations are modular in the sense that each sub-expression is encoded into a set of clauses whose structure is independent of how the expression is used. For example, an SMT solver can use the same template to generate clauses for every occurrence of a 64-bit multiplication operation.

For most non-trivial expressions, there are many different encodings available. For example, there are several ways to encode cardinality constraints [1, 4, 37]. These may use different clauses and possibly introduce auxiliary variables to simplify and compact the encodings. The choice of encoding can have a significant impact on the performance of the solver [35]. This difference can be large enough that identifying a bad encoding from the CNF it generates and then replacing it with a better one within the SAT solver can give a net improvement in solver performance [34]. Despite the importance of choosing a good encoding there remain open questions about why some encodings perform better than others. A common rule of thumb is that smaller encodings (primarily in terms of number clauses but also in the number of variables) are preferable. For some kinds of encoding, for example cardinality constraints, arc consistency [24] is regarded to be a desirable property. Another desirable property is being propagation complete [11]. Encodings with this property are considered extremely important since constraint solvers can benefit from the increase in inference power. However, its use is not yet wide spread in encoding design within the SMT community.

These issues are particularly relevant in encodings of bit-vector and floating-point operations. Often the only way to tell if an encoding might be better than another is to implement it and then compare system level performance on a ‘representative’ set of benchmarks. Furthermore, the encodings commonly used are frequently literal translations of circuits designs used to implement these operations in hardware. These designs were created to minimise signal propagation delay, to reduce area or for power and layout concerns. It is not clear why a multiplier hardware design with low cycle count should give a good encoding from bit-vector logic to CNF.

This paper advances both the theory and practice of the creation of encodings through the following contributions:

• Section 3 uses and extends the framework of abstract satisfiability [19] to formalise one aspect of encoding quality: propagating strength. We show that propagation complete encodings [11] are modelled by our framework and can serve as a basis for comparing encodings.

• An algorithm is given in Sect. 4 which can be used to determine if an encoding is propagation complete, strengthen it if it is not or generate a propagation complete encoding from scratch with and without auxiliary variables.

• In Sect. 5 we show that using our propagation complete encodings improves the performance of the CVC4 SMT solver on a wide range of bit-vector benchmarks.

2 Abstract Satisfaction

The abstract satisfaction framework [19] uses the language of abstract interpretation to characterise and understand the key components in a SAT solver [17]. One advantage of this viewpoint is that it is largely independent of the concrete domain that is being searched (sets of assignments) or the abstract domain used to represent information about the search (partial assignments). This allows the CDCL algorithm to be generalised [18] and applied to a range of other domains [12, 20, 27]. Another important feature of the abstract satisfaction framework is that it allows the representation of a problem and the effects of reasoning to be cleanly formalised. As we show later, this allows us to characterise propagation algorithms, such as unit propagation, as a map from representation to effect. In this section we recall some background results required to formalise this idea.

The foundation of abstract interpretation is using an abstract domain to perform approximate reasoning about a concrete domain. This requires a relation between the two domains; with Galois connections being one of the simplest and most popular choices.

Definition 1

Let $(C, \subseteq )$ and $(A, \sqsubseteq )$ be sets with partial orders. The pair $(\alpha : C \rightarrow A, \gamma : A \rightarrow C)$ form a Galois connection if:

$$\begin{aligned} \forall c \in C, a \in A \centerdot \alpha (c) \sqsubseteq a \Leftrightarrow c \subseteq \gamma (a) \end{aligned}$$

C is referred to as the concrete domain and A is the abstract domain. It is sometimes useful to use an equivalent definition of Galois connection: $\alpha$ and $\gamma$ are monotone and

$$\begin{aligned} \forall c \in C \centerdot c \subseteq \gamma (\alpha (c))&&\forall a \in A \centerdot \alpha (\gamma (a)) \sqsubseteq a \end{aligned}$$

If, additionally, $\gamma \circ \alpha = id$, then the pair is referred to as a Galois insertion and each element of the concrete domain has one or more representations in the abstract domain.

Given the domain that we want to reason about and the abstraction that will be used to perform the reasoning, the next step is to characterise the reasoning as transformers.

Definition 2

A concrete transformer is a monotonic function $f : C \rightarrow C$. Many of the transformers of interest are extensive, reductive or idempotent, respectively defined as:

$$\begin{aligned} \forall c \in C \centerdot c \subseteq f(c)\quad \forall c \in C \centerdot f(c) \subseteq c \quad f \circ f = f \end{aligned}$$

A function that is extensive, monotonic and idempotent is referred to as an upper closure while a reductive, monotonic, idempotent function is referred to as a lower closure.

Finally, we will need a means of approximating the transformer on the abstract domain using an abstract transformer. This gives a key result: the space of abstract transformers (for a given concrete transformer) forms a lattice with a unique best abstract transformer.

Definition 3

Given a transformer f on C, $f_o : A \rightarrow A$ is an (over-approximate) abstract transformer if:

$$\begin{aligned} \forall a \in A \centerdot \alpha (f(\gamma (a))) \subseteq f_o(a) \end{aligned}$$

Proposition 1

Given a reductive transformer f on a lattice $(C, \subseteq )$, the set of abstract transformers on lattice $(A, \sqsubseteq )$ form a lattice with the bottom element, referred to as the best abstract transformer, is equal to:

$$\begin{aligned} \alpha \circ f \circ \gamma \end{aligned}$$

3 Characterising Propagating Strength

While the framework we introduce in this section generalizes to other domains, we will focus on CNF encodings targeting CDCL-style SAT solvers [9]. We only consider unit propagation, but other propagation algorithms, such as generalised unit propagation [33], can be treated in the same way.

A number of attributes can be used for evaluating encodings. Some of these are algorithmic such as how much information it can propagate, how it affects the quality of learnt clauses, how it interacts with the branching heuristic or what effect it has on preprocessing. Others are more implementation-oriented: how many variables it uses, how many clauses it contains and how many are binary, ternary, how quickly it propagates, etc. In this work we will be characterising one of the major algorithmic properties: the amount of information that can be propagated.

Informally, this can be thought of as the proportion of facts that are true (with respect to the current partial assignment and encoding) that can be proven with unit propagation. If $\mathsf {E}$ is an encoding, l is a literal and $\mathsf {p}$ is a partial assignment expressed as a conjunct of all of the assigned literals, then it is the degree to which:

$$\begin{aligned} \mathsf {p} \wedge \mathsf {E} \models l &\text {implies}& \mathsf {p} \wedge \mathsf {E} \vdash _{up} l, \end{aligned}$$

where $\models$ represents logical entailment and $\vdash _{up}$ stands for unit propagation.

Fig. 1.

A graphical presentation of the results in Sect. 3

Fig. 2.

A nest of adders

We formalise this intuition using the viewpoint of abstract satisfaction. Figure 1 gives a visual summary of the formalisation; the key steps are:

• 1. Present syntax as an abstraction of semantics and define the space of encodings of a set of assignments as a substructure of the syntax lattice (Subsect. 3.1).

• 2. Show that partial assignments, the information about possible models that is manipulated during the search, is also an abstraction of the semantics (Subsect. 3.2).

• 3. Express the effects of reasoning as abstract transformers and characterise propagation algorithms such as unit propagation as maps from representations of a problem to the effects of reasoning (Subsect. 3.3).

3.1 Syntax and Semantics

We first fix a set of variable names $\varSigma$. This will include the ‘input’ and ‘output’ bits of the encoding, plus any auxiliaries. Let $\varSigma ^{+}$ be the set of literals constructed from these variables (i.e. $\varSigma ^{+}= \{ v |v \in \varSigma \} \cup \{ \lnot v |v \in \varSigma \}$). For simplicity we will assume double negation is always simplified $\lnot \lnot v = v$.

A clause is a disjunction of one or more literals. For convenience we will identify clauses with the set of literals they contain. A clause is a tautology if it contains a literal and its negation. Let $\mathscr {C}_{\varSigma ^{+}}$ be the set of non-tautological clauses which can be constructed from $\varSigma ^{+}$. We identify sets of clauses with their conjunction. Let $2^{\mathscr {C}_{\varSigma ^{+}}}$ denote the powerset of $\mathscr {C}_{\varSigma ^{+}}$ and note that it forms a complete lattice ordered by $\supseteq$. For convenience we will pick $\emptyset$ to be the top element and $\mathscr {C}_{\varSigma ^{+}}$ to be the bottom.

Example 1

We will use a full adder as a running example. Figure 2 shows one possible circuit that can be used to implement a full adder as well as the truth table for the input which gives the 8 possible satisfying assignments of the formula. In this case $\varSigma = \{a, b, c_{in}, s, c_{out}\}$ so $\varSigma ^{+}= \{a, b, c_{in}, s, c_{out}, \lnot a, \lnot b, \lnot c_{in}, \lnot s, \lnot c_{out}\}$. Thus $\{a\}$, $\{b, \lnot a\}$, $\{s, \lnot s\}$ are clauses and only the last is a tautology. Also $\mathscr {C}_{\varSigma ^{+}} = \{\emptyset , \{a\}, \{b\}, \{\lnot a\}, \{a, b\}, \{a, \lnot b\}, \dots \}$.

An assignment is a map from $\varSigma$ to $\{\top , \bot \}$ and the set of all assignments is denoted by $\mathscr {A}_{\varSigma }$. Similarly $2^{\mathscr {A}_{\varSigma }}$ forms a powerset lattice. Following usual convention (and the opposite of the syntax lattice), the top element will be $\mathscr {A}_{\varSigma }$ and $\emptyset$ the bottom. With a slight abuse of notation, we use assignments to give literals values: $\mathsf {x} (\lnot a) = \lnot \mathsf {x} (a)$.

The models relation, denoted using an infix $\models$, is a relationship between $\mathscr {A}_{\varSigma }$ and $\mathscr {C}_{\varSigma ^{+}}$, defined as follows:

$$\begin{aligned} \mathsf {x} \models c \Leftrightarrow \exists l \in c \centerdot \mathsf {x} (l) = \top \end{aligned}$$

An assignment is a model of a set of clauses if the models relation holds for all of the clauses in the set.

Example 2

An assignment for the full adder example would be:

$\mathsf {x} = \{(a,\top ), (b,\top ), (c_{in},\bot ), (c_{out},\top ), (s,\bot )\}$.

From this we can see that $\mathsf {x} \models \{a\}$ and $\mathsf {x} \models \{a, \lnot c_{in}, c_{out}\}$ but $\mathsf {x} \not \models \{\lnot b, \lnot a\}$. So $\mathsf {x}$ is a model of $\{\{a\}, \{a, \lnot c_{in}, c_{out}\}\}$.

This relation gives maps $\mathsf {AofC} : 2^{\mathscr {C}_{\varSigma ^{+}}} \rightarrow 2^{\mathscr {A}_{\varSigma }}$ and $\mathsf {CofA} : 2^{\mathscr {A}_{\varSigma }} \rightarrow 2^{\mathscr {C}_{\varSigma ^{+}}}$:

$$\begin{aligned} \mathsf {AofC}(C)= & {} \{ \mathsf {x} \in \mathscr {A}_{\varSigma } |\forall c \in C \centerdot \mathsf {x} \models c \} \\ \mathsf {CofA}(A)= & {} \{ c \in \mathscr {C}_{\varSigma ^{+}} |\forall \mathsf {x} \in A \centerdot \mathsf {x} \models c \} \end{aligned}$$

$\mathsf {AofC}(C)$ is the set of assignments which are models of C, while $\mathsf {CofA}(A)$ is all of the clauses that are consistent with all of the assignments in A. Both maps are monotonic, $\mathsf {AofC}(\mathsf {CofA}(A)) = A$ and $\mathsf {CofA}(\mathsf {AofC}(C)) \supseteq C$ so they form a Galois insertion between $2^{\mathscr {A}_{\varSigma }}$ and $2^{\mathscr {C}_{\varSigma ^{+}}}$. A set of clauses is a representation, or abstraction, of its set of models.

Example 3

Given $C = \{\{a, \lnot b\}, \{\lnot a\}\}$, the set of all models of C is $\mathsf {AofC}(C) = \{ \mathsf {y} : \varSigma \rightarrow \{\top , \bot \} |\mathsf {y} (a) = \bot \wedge \mathsf {y} (b) = \bot \}$. Conversely, $\mathsf {CofA}(\{\mathsf {x} \}) = \{ \{a\}, \{a, b\}, \{a, \lnot b\},$ $\dots \}$ is the set containing all of the clauses consistent with the assignment $\mathsf {x}$ from Example 2. When multiple assignments are given this is all of the clauses that are consistent with all of the assignments.

Fig. 3.

A nest of adder encodings

In the SAT field, similar Galois connections to the one presented in this section have been studied in [32]. Although we have presented this result with Boolean valuations (the “concrete” domain) and CNF (the “abstract” domain), the construction is much more general and can be applied to SMT, CSP, ASP, etc. For more discussion of the Galois connection between syntax and semantics, see [21].

Given a set of assignments $M \subset \mathscr {A}_{\varSigma }$, an encoding (of M) is any set of clauses $C \subset \mathscr {C}_{\varSigma ^{+}}$ such that $\mathsf {AofC}(C) = M$. We shall denote the set of encodings of M as $\mathscr {E}_{M} = \{ C \subset \mathscr {C}_{\varSigma ^{+}} |\mathsf {AofC}(C) = M \}$. If C and D are both encodings (of the same set of models), then so is $C \cup D$; this is the basis for redundant encodings in CSP. It also implies that the encodings of a set of models form a meet semi-lattice with a minimum element, $\mathsf {CofA}(M)$, the most verbose encoding. There can be multiple, incomparable, least verbose encodings. For example if $M = \emptyset$, then $\{{a}, {\lnot a}\}$ is a least verbose encoding (as there are no proper subsets which are encodings), but so is $\{{b}, {\lnot b}\}$. This notion of encoding has been studied is the SAT field (e.g. [23]) and has recently been formalised as a formula that has the same satisfying assignments as the set of assignments of a given specification [26].

Example 4

Continuing our example of a full adder, let M be the set of eight models described by the truth table in Fig. 2a. There are many possible encodings, some of which are given in Fig. 3. All of these are subsets of $\mathsf {CofA}(M)$, all the clauses consistent with M, in effect, the ‘theory’ of the full adder. However, not every subset of $\mathsf {CofA}(M)$ is an encoding, as they are required to have the same models as M. Possible encodings include the naive encoding (Fig. 3a) in which all full assignments that are not models are removed, the basic encoding given by [23] (Fig. 3b) and a propagation complete encoding (Fig. 3c). Notice that the first two encodings are not propagation complete.

To formally define propagation strength, we will need a notion of what kind of information we are propagating and to relate the encoding to the action of propagation.

3.2 Representing Information During Search

Some propositional logic tools, such as BDDs, represent sets of models directly. For solving SAT problems this is not really viable — as soon as you have a model that you could represent, you have solved the problem. Thus SAT algorithms need a way of representing partial information about models. For example if an encoding contains the clause $\{\lnot a\}$ then the SAT solver needs a way of recording “there are no models that assign a to $\top$”. The most common approach is to use partial assignments.

Following [17] we characterise a partial assignment over $\varSigma$ ($\mathscr {P}_{\varSigma }$ denotes the set of all of them) as an abstraction of $2^{\mathscr {A}_{\varSigma }}$. Partial assignments are maps from $\varSigma$ to $\{\top , ?, \bot \}$, where ? denotes an unknown or unassigned variable. They can be ordered by:

$$\begin{aligned} \mathsf {p} \sqsubseteq \mathsf {q} \Leftrightarrow \forall v \in \varSigma . \mathsf {q} (v) \not =? \Rightarrow \mathsf {p} (v) = \mathsf {q} (v) \end{aligned}$$

Allowing an additional ‘contradiction’ partial assignment, $\bot ^{\mathscr {P}}$, ordered below all other partial assignments, makes $\mathscr {P}_{\varSigma }$ a complete lattice, where $\top ^{\mathscr {P}} = \lambda v.?$ is the partial assignment that does not assign any variables. The discussion below generalises to other abstractions; we use partial assignments as they are a popular and simple choice.

Example 5

In our running example, $\mathsf {p}$ and $\mathsf {q}$ are partial assignments:

$$\begin{aligned} \mathsf {p}= & {} \{(a,?), (b,\bot ), (c_{in}, \bot ), (s,\top ), (c_{out},\top )\} \\ \mathsf {q}= & {} \{(a,?), (b,?), (c_{in},?), (s,\top ), (c_{out},\top )\} \end{aligned}$$

with $\mathsf {p} \sqsubseteq \mathsf {q}$ because where $\mathsf {q}$ assigns a variable to $\top$ or $\bot$, $\mathsf {p}$ agrees.

To use $\mathscr {P}_{\varSigma }$ as an abstraction of $2^{\mathscr {A}_{\varSigma }}$, we need to define a Galois connection between them. Let $\alpha : 2^{\mathscr {A}_{\varSigma }} \rightarrow \mathscr {P}_{\varSigma }$ denote the map from models to the most complete partial assignment that is consistent with all of them and $\gamma : \mathscr {P}_{\varSigma } \rightarrow 2^{\mathscr {A}_{\varSigma }}$ denote the map from a partial assignment to the set of models that is consistent with it:

$$\begin{aligned} \alpha (A) = \bigsqcup _{\mathsf {x} \in A} x&&\gamma (\mathsf {p}) = \{ \mathsf {x} \in \mathscr {A}_{\varSigma } |\forall v \in \varSigma \centerdot \mathsf {p} (v) \not =? \Rightarrow \mathsf {x} (v) = \mathsf {p} (v) \} \end{aligned}$$

Example 6

Let $\mathsf {x} _1, \mathsf {x} _2, \mathsf {x} _3$ and $\mathsf {x} _4$ be (full) assignments:

$$\begin{aligned} \mathsf {x} _1= & {} \{(a, \top ), (b, \top ), (c_{in}, \bot ), (s, \bot ), (c_{out}, \top )\} \\ \mathsf {x} _2= & {} \{(a, \top ), (b, \bot ), (c_{in}, \top ), (s, \bot ), (c_{out}, \top )\} \\ \mathsf {x} _3= & {} \{(a, \top ), (b, \top ), (c_{in}, \top ), (s, \bot ), (c_{out}, \top )\} \\ \mathsf {x} _4= & {} \{(a, \top ), (b, \bot ), (c_{in}, \bot ), (s, \bot ), (c_{out}, \top )\} \end{aligned}$$

then:

$$\begin{aligned} \alpha (\{\mathsf {x} _1, \mathsf {x} _2\})= & {} \{(a, \top ), (b, ?), (c_{in}, ?), (s, \bot ), (c_{out}, \top )\} \\ \gamma (\alpha (\{\mathsf {x} _1, \mathsf {x} _2\}))= & {} \{\mathsf {x} _1, \mathsf {x} _2, \mathsf {x} _3, \mathsf {x} _4\} \end{aligned}$$

3.3 Effects of Reasoning

Having defined partial assignments as the ‘units’ of information that propagation uses, the next step is to formalize what kind of reasoning we are performing. In a SAT solver the role of reasoning is to add to a partial assignment $\mathsf {p}$ (i.e., reduce the set of assignments that is being considered) that is consistent with all of the models in $\gamma (\mathsf {p})$. Formally, this is expressed in two steps: a models transformer on the concrete domain, $2^{\mathscr {A}_{\varSigma }}$, which captures the kind of reasoning that we are approximating and abstract transformers on $\mathscr {P}_{\varSigma }$, which express the actual changes to the partial assignments.

In slight variation from [18] we define the models transformer, $\mathsf {mod}_{M} : 2^{\mathscr {A}_{\varSigma }} \rightarrow 2^{\mathscr {A}_{\varSigma }}$, as parameterised by a set of assignments rather than a formula:

$$\begin{aligned} \mathsf {mod}_{M}(A) = M \cap A \end{aligned}$$

This is a downward closure function on $2^{\mathscr {A}_{\varSigma }}$ and expresses the ideal reasoning, or, conversely, the limit of what is sound.

Example 7

In the full adder example, let M be the set of assignments described in the truth table in Fig. 2a. If $A = \{\mathsf {x} _1, \mathsf {x} _2, \mathsf {x} _3, \mathsf {x} _4\}$, then $\mathsf {mod}_{M}(A) = \{\mathsf {x} _1, \mathsf {x} _2\}$ as these are the only two assignments in A that are also models of the full adder.

As $2^{\mathscr {A}_{\varSigma }}$ is not directly representable for problems of significant size, we use $\mathscr {P}_{\varSigma }$. Likewise, we cannot directly implement $\mathsf {mod}_{M}$ so instead we must use over-approximate transformers on $\mathscr {P}_{\varSigma }$. Let $\mathscr {T}_{\mathsf {mod}_{M}}$ denote the set of abstract transformers that over-approximate $\mathsf {mod}_{M}$ and recall from Proposition 1 that they can be ordered point-wise to form a lattice with id as the top element and $\alpha \circ \mathsf {mod}_{M} \circ \gamma$ as the bottom. The effect of a sound propagator or other form of reasoning should be an abstract transformer, as they soundly add to partial assignment.

The final link is to connect the encoding used to the effect of reasoning. To do this we consider the unit propagation algorithm as a map from $\mathsf {UP} : \mathscr {E}_{M} \rightarrow (\mathscr {P}_{\varSigma } \rightarrow \mathscr {P}_{\varSigma })$ that uses a set of clauses to add assignments to a partial assignment.

Definition 4

Let $\mathsf {up} : \mathscr {C}_{\varSigma ^{+}} \rightarrow (\mathscr {P}_{\varSigma } \rightarrow \mathscr {P}_{\varSigma })$ map clauses to functions on partial assignments.

$$\begin{aligned} assign(l)= & {} \lambda k . {\left\{ \begin{array}{ll} \top &{} k = l \\ \bot &{} k = \lnot l \\ ? &{} \text {otherwise} \end{array}\right. } \\ \mathsf {up}(c)= & {} \lambda p . {\left\{ \begin{array}{ll} p \sqcap assign(l) &{} \exists l \in c \centerdot p(l) = ? \wedge \forall k \in c \centerdot k \not =l \Rightarrow p(k) = \bot \\ p &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

Define $\mathsf {UP}$ as the (greatest) fix-point of applying $\mathsf {up}(c)$ for each clause in the encoding:

$$\begin{aligned} \mathsf {UP}(C)(p) = \text {GFP}\left( \lambda q . p \sqcap (\sqcap _{c \in C} \mathsf {up}(c)(q))\right) \end{aligned}$$

Example 8

Given the set C clauses in Fig. 3b we have:

$$\begin{aligned} \mathsf {UP}(C)(\{(a,\top ), (b,\top ), (c_{in}, \top ), (s, ?), (c_{out}, ?)\})= & {} \\ \{(a,\top ), (b,\top ), (c_{in}, \top ), (s, \top ), (c_{out}, \top )\}) \end{aligned}$$

as the clause $\{\lnot a, \lnot b, c_{out}\}$ assigns $c_{out}$ to $\top$ and $\{\lnot a, \lnot b, \lnot c_{in}, s\}$ assigns s to $\top$.

Formalised in this manner, $\mathsf {UP}$ has a number of useful order-theoretic properties:

Proposition 2

Given $C, D \subset \mathscr {C}_{\varSigma ^{+}}$, $\mathsf {UP}(C_i)$ is a closure function as:

$$\begin{aligned} \mathsf {UP}(C) \leqslant id& C \leqslant D \implies \mathsf {UP}(C) \leqslant \mathsf {UP}(D) &\mathsf {UP}(C) \circ \mathsf {UP}(C) = \mathsf {UP}(C) \end{aligned}$$

Note that $\mathsf {UP}$ is neither injective ($\mathsf {up}(\{\{a\}, \{b\}\}) = \mathsf {up}(\{\{a\}, \{b\}, \{\lnot a, b\}\})$) nor surjective. Furthermore, $\mathsf {UP}$ does not preserve meets (well defined on encodings) or joins (partially defined on encodings, fully defined on supersets of a given encoding). A propagation algorithm that preserves joins would give a Galois connection between supersets of an encoding and abstract transformers, thus giving a unique, minimal encoding required to give a certain amount of inference.

The final step is to show that the closure functions given by $\mathsf {UP}(C)$ are abstract transformers and that they include the best abstract transformer.

Theorem 1

Let $M \in 2^{\mathscr {A}_{\varSigma }}$ be a set of assignments then:

$$\begin{aligned} \{ \mathsf {UP}(C) | C \in \mathscr {E}_{M} \} \subseteq \mathscr {T}_{\mathsf {mod}_{M}}&&\mathsf {UP}(\mathsf {CofA}(M)) = \alpha \circ \mathsf {mod}_{M} \circ \gamma \end{aligned}$$

Thus an encoding $C \in \mathscr {E}_{M}$ is a propagation complete encoding (PCE) [11] when:

$$\begin{aligned} \mathsf {UP}(C) = \alpha \circ \mathsf {mod}_{M} \circ \gamma \end{aligned}$$

Propagation complete encodings (PCEs) are not unique and there may be many, incomparable PCEs. One goal of encoding design can be the creation of PCEs with other desirable properties, such as using a minimal number of clauses or auxiliary variables. As with clauses, assignments and partial assignments, the discussion above is more general than unit propagation alone. Using our abstract satisfaction framework we can model PCEs. In the next section we present an algorithm for automatically generating PCEs.

4 Generating Propagation Complete Encodings

The previous section defined the notion of propagation complete encodings (PCEs) within our framework. Next, we present an algorithm (Algorithm 1) that can be used to determine if an encoding is propagation complete, strengthen it if not, and generate a PCE that is equisatisfiable to a reference encoding. Algorithm 1 takes as input a set of variables $\varSigma$ that will serve as the encoding vocabulary, an initial encoding $\mathsf {E} _0$ and a reference encoding $\mathsf {E_{Ref}}$ (over a vocabulary including $\varSigma$), such that $\mathsf {AofC}(\mathsf {E_{Ref}}) = M$. Note that, if $\mathsf {E} _0 = \emptyset$, then the algorithm will build a PCE over $\varSigma$ from scratch that is equisatisfiable to $\mathsf {E_{Ref}}$. In practice $\mathsf {E} _0 = \emptyset$, and $\mathsf {E_{Ref}}$ can be any encoding of the circuit.

The algorithm traverses the fix-points of the best abstract transformer $\alpha \circ \mathsf {mod}_{M}\circ \gamma$, i.e. partial assignments where no new facts can be deduced. To achieve this, the algorithm uses a priority queue ($\mathsf {PQ}$) of partial assignments sorted by partial assignment size. For each element of $\mathsf {PQ}$, we examine the variables v that unit propagation cannot infer from $\mathsf {E}$ and $\mathsf {pa}$ (line 5). We then check if the reference encoding $\mathsf {E_{Ref}}$, along with the current partial assignment $\mathsf {pa}$ logically entail either v or $\lnot v$. This check is done via a call to a SAT oracle at line 8 (in our implementation this is a call to a CDCL SAT solver). If the query returns $sat$, the variable is not entailed and the extended partial assignment is added to the queue. Otherwise, l was a missed propagation and the encoding is strengthened by adding a clause that blocks the partial assignment $\mathsf {pa}$.¹

If two partial assignments $\mathsf {q_1}$ and $\mathsf {q_2}$ unit propagate the same literals ($\mathsf {UP}(\mathsf {E})(\mathsf {q_1}) = \mathsf {UP}(\mathsf {E})(\mathsf {q_2})$) we only need to explore extensions of one of them. Therefore, the $\mathsf {push}$ operation on line 9 only adds $\mathsf {pa} '$ to $\mathsf {PQ}$ if $\forall \mathsf {q} \in \mathsf {PQ} \centerdot \mathsf {UP}(\mathsf {E})(\mathsf {q}) \ne \mathsf {UP}(\mathsf {E})(\mathsf {pa})$. In other words we cache assignments that become equal when extended by unit propagation. Because we are potentially strengthening the encoding $\mathsf {E}$ with each iteration of the for-loop the amount of information unit propagation can infer from $\mathsf {E}$ increases. The $\mathsf {PQ}$.$\mathsf {compact}$ call on line 12 iterates over the queue elements and removes queue elements that $\mathsf {UP}$-extend to the same partial assignment. This ensures the invariant at the beginning of the while-loop. Furthermore, at the end of the while loop the current encoding $\mathsf {E}$ is strong enough to unit propagate all literals entailed from $\mathsf {pa}$. The continuous strengthening of $\mathsf {E}$ also reduces the number of unassigned variables explored at line 5.

The algorithm is not always guaranteed to generate subset-minimal encodings. The order in which the partial assignments is considered may lead to the learning of redundant clauses. A clause c is redundant w.r.t. a PCE $\mathsf {E_{PC}}$ if for all literals $l\in c$ unit propagation can infer l from $\mathsf {E_{PC}} \setminus c$ assuming the negation of the other literals $\lnot (c\setminus \{l\})$. For example, in the presence of a chain of implications, $v_1 \Rightarrow v_2 \Rightarrow \ldots \Rightarrow v_k$, the algorithm may learn the redundant clause $c = \{\lnot v_1, v_k\}$. Note that c is redundant since $v_1 \wedge (\mathsf {E_{PC}} \setminus c) \vdash _{up} v_k$ and $\lnot v_k \wedge (\mathsf {E_{PC}} \setminus c) \vdash _{up} \lnot v_1$. For this reason, after running Algorithm 1 we use the minimisation procedure described in [11] to remove redundant clauses while maintaining propagation completeness.

Auxiliary Variables. The algorithm we described so far only works on a fixed vocabulary $\varSigma$ consisting of the input and output variables of the encoding. For certain operators, there no polynomially-sized CNF encodings if we restrict ourselves to the input/output variables only. For this reason, we extended our algorithm to further reduce the size of the encoding while maintaining propagation completeness by heuristically adding auxiliary variables. Given a set of auxiliary variables $\mathsf {Aux}$, we extend the reference encoding $\mathsf {E_{Ref}}$ by adding the definitional clauses $\mathsf {Def} (\mathsf {aux})$ for each auxiliary variable $\mathsf {aux} \in \mathsf {Aux}$: $\mathsf {Def} (\mathsf {aux}) \wedge \mathsf {E_{Ref}}$. For example, to introduce an auxiliary variable $a\equiv x\wedge y$ for inputs x, y, we add the clauses corresponding to the formula $a \Leftrightarrow (x \wedge y)$ to $\mathsf {E_{Ref}}$ and run Algorithm 1 on $\varSigma \cup \{a\}$.

We implemented a greedy algorithm that iteratively repeats this process as shown in Algorithm 2. We denote by $\mathsf {genPCE}$ the procedure of generating a propagation complete encoding from a reference encoding given in Algorithm 1. We denote by $|\mathsf {E}|$ the size of an encoding as the number of clauses. The algorithm takes as input a reference encoding $\mathsf {E_{Ref}}$, a fixed alphabet $\varSigma$ as well as a set of auxiliary variables $\mathsf {Aux}$. It initially computes the PCE over the input/output variables $\varSigma$. For each auxiliary variable $\mathsf {aux}$ in the current set of auxiliary variables, it computes the PCE over the alphabet $\varSigma \cup \{\mathsf {aux} \}$ from reference encoding $\mathsf {E_{Ref}} \wedge \mathsf {Def} (\mathsf {aux})$, where $\mathsf {Def} (\mathsf {aux})$ is the set of definitional clauses for $\mathsf {aux}$. It then chooses the auxiliary variable $\mathsf {best}$ that minimises the encoding the most, and adds it to the reference encoding. The process is repeated on the remaining auxiliary variables $\mathsf {Aux} \setminus \{\mathsf {aux} \}$ until no minimisation is achieved. Note that this is a greedy algorithm, and does not guarantee finding a minimal size encoding w.r.t. the given auxiliary variables. For the set of potential auxiliary variables $\mathsf {Aux}$, we generate Boolean combinations over the input/output variables up to a limited depth. As a heuristic, we also add to the set $\mathsf {Aux}$ the auxiliary variables used by the reference encoding.

Fig. 4.

Composition of encoding primitives to build a n-bit less than comparator.

Generating Propagation Complete Encodings. Algorithm 1 solves an inherently hard problem and may call a SAT solver an exponential number of times. It is intended to be used as a tool to support encoding design rather than generating complete encodings.

To explore the feasibility of generating PCEs, we analysed the propagation completeness of encodings used in the CVC4 SMT solver [5]. CVC4 uses small circuit primitives to build more complex encodings of word-level bit-vector operators. Figure 4 shows an example of how small circuits for unsigned less than ($a < b$) primitives can be composed to build a more complex encoding to compare n-bit bit-vectors. Each unsigned less than comparator (ULT) has three input bits (a, b, r) and one output bit (o). There are different ways that this primitive can be encoded into CNF. A possible PCE is: $\{\{o, \lnot b, a\},$ $\{o, \lnot b, \lnot r\},$ $\{a, \lnot r, o\},$ $\{\lnot o, b, \lnot a\}, \{\lnot o, r, \lnot a\},\{\lnot o, r, b\}\}$. If r has value $\bot$, then o will be $\top$ iff $a < b$. Otherwise, if r has value $\top$, then o will be $\top$ iff $a \le b$. This structure allows the ULTs to be chained together to form an n-bit PCE for the ULT comparator. A similar construction can be done for other encoding primitives and is common in circuit design. For example, full-adders can be chained to form a ripple-carry adder. Note that, if the encoding primitives are not PC, then their composition will not be PC. However, the converse does not necessarily hold.

Table 1 shows the size of the encodings generated by Algorithm 1 and by introducing auxiliary variables compared to the size of the reference encoding $\mathsf {E_{Ref}}$, starting with an empty initial encoding $\mathsf {E} _0$. As encoding primitives (prim), we have considered the if-then-else operator ($\mathsf {ite}$-$\mathsf {gadget}$), an unsigned less than comparator ($\mathsf {ult}$-$\mathsf {gadget}$), a signed less than comparator ($\mathsf {slt}$-$\mathsf {gadget}$), the full-adder ($\mathsf {full}$-$\mathsf {add}$), adder with base 4 ($\mathsf {full}$-$\mathsf {add}$-$\mathsf {base4}$), bit-count circuits ($\mathsf {bc3to2}$, $\mathsf {bc7to3}$), 2 x 2 multiplication circuit ($\mathsf {mult2}$), and multiplication by a constant ($\mathsf {mult}$-$\mathsf {const3}$, $\mathsf {mult}$-$\mathsf {const5}$, $\mathsf {mult}$-$\mathsf {const7}$). These encoding primitives are then composed (comp) to build n-bit bit-vector operators.

Table 1. Generation of PCEs for small encoding primitives and their composition

These experiments were run on Intel Xeon X5667 processors (3.00 GHz) running Fedora 20 with a timeout of 3 h and a memory limit of 32 GB. In case of timeout of the greedy algorithm, we present the smallest encoding found until the timeout. The reference encodings used were the default implementations in CVC4. From the encoding primitives presented in Table 1, $\mathsf {ite}$ is the only encoding primitive that is propagation complete in CVC4. This scenario is not restricted to CVC4, and most state-of-the-art SMT solvers do not build PCEs (see Sect. 5 for further details).

For small primitives our algorithms can easily find PCEs with small size even when restricting the set of variables to inputs and outputs. For more complex circuits, as mult-4bit, the PCE can be much larger than the non-PCE. When generating PCEs with $\varSigma$ containing auxiliary variables, we can obtain considerably smaller encodings. For example, for the addition operator $\mathsf {add}$-$\mathsf {4bit}$ the number of clauses decreased from 336 to 43 by only adding 3 auxiliary variables. In this case, the auxiliary variables that are added by our greedy algorithm correspond to the carry bits from the chained adders. Note that the PCE for $\mathsf {add}$-$\mathsf {4bit}$ formed by chaining the propagation complete full-adder results in an encoding with 20 variables and 60 clauses, which has a similar size to the PCE found by our greedy algorithm.

Even though the algorithm can take a considerable amount of time to find small PCEs with auxiliary variables, our goal is not to apply such algorithm to large formulae but only to find PCEs of primitives. This process is done once, offline. Afterwards, the encoding primitives can be chained together to form larger encodings for any bit-width. We verified with our algorithm that for small bit-widths the composition of PCEs for adders and comparators is propagation complete, while for the multiplier is not. We conjecture that the existence of a reasonably-sized propagation complete multiplier is unlikely, as this would help to efficiently solve hard factorization problems.

5 Experimental Evaluation

To explore the impact of propagation strength on performance, we implemented the PCE primitives generated in Sect. 4 in the CVC4 SMT solver [5]. CVC4 is a competitive solver that ranked 2nd in the 2015 SMT-COMP bit-vector division. We instrumented the solver’s bit-blasting procedure to use the primitives to build more complex encodings of word-level bit-vector operators.

Fig. 5.

The impact of using PC primitives in various kinds of multiplication circuits

We focused on the following bit-vector operators: comparison, addition and multiplication. The rest of the bit-vector operations were either already propagation complete (e.g. bitwise and), or could be expressed in terms of other operations. We implemented n-bit circuits using the primitives described in Sect. 4. For addition, we used the propagation complete $\mathsf {full\text {-}adder}$ (cvcAO) and for comparison the $\mathsf {ult\text {-}gadget}$ and $\mathsf {slt\text {-}gadget}$ (cvcLO). For multiplication we implemented variants that use PC primitives: shift-add multiplication (cvc vs cvcMO), tree reduction (cvcT vs cvcTO) and multiplication by blocking (cvcB2 vs cvcB2O). We append $\mathsf {O}$ to the solver’s name to denote that the propagation complete sub-circuits are enabled. All implementations of multiplications that use propagation complete sub-circuits use the PC $\mathsf {full\text {-}adder}$ for adding the partial products, while blocking multiplication also uses the propagation complete 2 by 2 multiplication sub-circuit $\mathsf {mult2}$.

We used 31066 quantifier-free bit-vector benchmarks from SMT-LIB v2.0  [6]. Experiments in this section were run on the $\mathsf {StarExec}$  [38] cluster infrastructure on Intel Xeon E5-2609 processors (2.40 GHz) running Red Hat Enterprise Linux Workstation release 6.3 (Santiago) with a timeout of 600 s seconds and a memory limit of 200 GB.

Figure 5 quantifies the impact of the PC components in the various kinds of multiplication circuits we implemented. The scatter plots are on the entire 31066 set of benchmarks, and are on a log-scale. Each point is a benchmark, and the x and y-axis represent the time (seconds) taken by CVC4 to solve the benchmark with the given configuration. Using the propagation complete primitives (cvcMO, cvcTO and cvcB2O) consistently improves performance over their default implementations. Although the performance improvement is not dramatic, we believe it is consistent enough to show that propagation strength is an important characteristic of encodings. Since cvcMO had the best performance between multiplication circuits that use propagation complete sub-circuits, we considered this encoding for further evaluation.

Table 2. Comparison of performance of propagation complete encodings in CVC4

Table 2 gives the number of problems solved and the time taken to solve them for CVC4 without propagation complete primitives (cvc) and with propagation complete primitives, namely: shift-add multiplier (cvcMO); shift-add multiplier and full-adder (cvcAMO); and shift-add multiplier, full-adder and comparison (cvcALMO). Due to space constraints we removed rows where the number of problems solved by all configurations was the same (see Appendix for full table). Table 2 shows that adding each PC primitives increases performance, with the configuration using PC primitives for addition, comparison and multiplication (cvcALMO) solving the most.

We believe this improvement is not limited to CVC4 but will translate to other solvers as well. We examined the source code of other competitive SMT solvers, such as boolector  [13], stp2  [28], yices2  [22] and z3  [15], and their implementation of addition is not propagation complete. Therefore, although the notion of propagation complete encodings is not new, it is not widely applied to solver encoding design. Preliminary results from implementing the PC full-adder in the CBMC model-checker [14] also showed an improved performance. The improvement is also not limited to constraint solvers that use CDCL SAT solvers but is also expected for look-ahead SAT solvers [29]. These solvers are geared towards propagation and are even more likely to take advantage of the increased inference power than CDCL SAT solvers.

We have shown that the propagation complete encoding primitives our algorithm generated can be used to build encodings of bit-vector operators in an SMT solver. The results are promising considering we are only strengthening a small part of the overall problem. Furthermore the propagation complete encodings have been automatically generated from scratch, while the existing encodings had been optimized by hand. This highlights the importance of propagation complete encoding in encoding design and that our proposed framework can help practitioners improve encodings.

6 Related Work

The notion of propagation strength has been explored under various names such as unit refutation complete [16] and propagation complete encodings (PCEs) [11] in AI knowledge compilation. A formula is unit refutation complete [16] iff any of its implicates can be refuted by unit propagation. Here we refer to refutation as being the process of proving the implication $\mathsf {E} \models l$ by proving $\mathsf {E} \wedge \lnot l \models \bot$. Bordeaux et al. [10] consider variations of unit refutation complete encodings, such as its disjunctive closure and a superset of unit refutation complete encodings where variables can be existentially quantified and unit refutation concerns only implications from free variables. Gwynne and Kullmann [25] introduce a general hierarchy of CNF problems based on “propagation hardness” and generalise the notion of unit refutation complete encodings.

PCEs are a proper subset of refutation complete encodings [25] and have been introduced by Bordeaux and Marques-Silva [11] for finding encodings where only using unit propagation suffices to deduce all the literals that are logically valid. The authors reduce the problem of generating PCEs to iteratively solving QBF formulas. We consider PCEs using an abstract satisfaction framework and rely on a SAT solver’s efficient UP routine to check whether a clause is empowering. Since QBF is a PSPACE-complete problem, it is unclear that the approach from [11] would scale better than ours. Because [11] has no implementation that we are aware of, we cannot compare against them. Their framework can also support adding auxiliary variables to PCEs but this approach was not explored by the authors. Our approach supports generating encodings over a limited alphabet of auxiliary variables and includes an implementation and extensive experimental results that show performance gains. The work in [2] shows that checking whether a clause is empowering (it is entailed by the given CNF formula and it increases the propagation power of the formula) is co-NP complete. It also shows the existence of operations that have only exponential PCEs. This supports our targeting of small encoding primitives as opposed to n-bit circuits which is likely intractable.

Propagation completeness has also been considered in CSP (e.g. [3, 8]) because of its connection to Domain Consistency, also known as Generalised Arc Consistency (GAC): when a constraint is encoded into SAT over some Finite-Domain variables, if the encoding of the constraint is propagation complete, then unit propagation on the SAT encoding effectively finds the same implications as Domain Consistency. In CSP it is common to consider GAC over procedural propagators [3] of specific constraints. Propagators can also be decomposed into primitive constraints that can be translated to SAT [8]. GAC has been adopted in SAT [24] and many encodings have this property [1, 4, 37]. However, GAC is usually only enforced on input/output variables and not on auxiliary variables. PCEs consider a stronger notion of propagation strength since GAC is enforced on both input/output variables as well as on auxiliary variables.

Trevor Hansen’s PhD [28] (independently) touches on many of the techniques we have used. He considers both ‘bit-blasting’ encodings and forward propagators (algorithms that implement abstract transformers directly), but treats these as independent approaches, omitting the link we show in Sect. 3. Although he tests the propagators for propagation completeness and even generates clauses to improve the propagators, he does not use this approach to generate complete encodings, nor does he perform minimisation. The SMT solver Beaver [30] also computes pre-synthesised templates for bit-vectors operators which are optimised offline using logic synthesis tools such as the ABC logic synthesis engine [7]. However, these templates are only computed for predefined bit-widths and are not PC. Hansen makes use of Reps’ et al. [36] work on computing best abstract transformers via a lifted version of Stalmarck’s algorithm. Algorithm 1 similarly uses breadth-first traversal, but the key difference is in how and when the algorithms are used. In [36] and most applications of their work [31], the result of the best abstract transformer is computed on-line as part of a search. We compute an encoding that gives the best abstract transformer off-line as part of solver development.

7 Conclusion

By using the abstract satisfaction framework we can characterise the space of encodings, the effects of reasoning and the link between them. Propagation complete encodings allow an increase of inference power that can be exploited by CDCL SAT solvers. We have showed that these encodings are captured by our abstract satisfaction formalism which allows us to reason about them and their extensions (Sect. 3). It is possible to compute subset-minimal propagation complete encodings and for various key operations these are tractably computable and often smaller than conventional encodings. For more complex encodings, we have shown that greedily introducing auxiliary variables can generate significantly smaller propagation complete encodings (Sect. 4). Implementing these in the CVC4 SMT solver gives performance improvements across a wide range of benchmarks (Sect. 5). It is hoped that this work will contribute to a more theoretically rigorous approach to encoding design.

Linking encodings to abstract transformers has many possible applications. Abstract transformers are functions on ordered sets and are therefore partially ordered. This gives a way of comparing the propagation strength of different encodings or investigating the effects of pre and in-processing techniques. This is particularly important as for certain operators there are no polynomially sized PCEs. A quantitative measure of propagation strength is a useful practical alternative. Proof-theoretic measures can be expressed as properties of the syntactic representation lattice, for example proof length becomes path length. Likewise solver run-time is bounded by the length of paths in $\mathsf {UP}(2^{\mathscr {C}_{\varSigma ^{+}}})$. Finally, the abstract satisfaction viewpoint provides a means of exploring many interesting questions about composition of encodings and when they preserve propagation strength.