Solving a Logic Synthesis Puzzle via SAT/SMT
A few weeks ago, I was asked the following riddle:
Design a logic circuit with three inputs and three outputs, such that the outputs are the inverted inputs. You may use arbitrary many AND and OR gates, but at most two NOT gates
.
Although the characterisation of this problem as an SMT instance is straightforward, I found it necessary to reduce it to SAT and incorporate further assumptions to achieve reasonable performance.
This post illustrates said process, ranging from the original idea to a standard formulation of SATbased logic synthesis to a problemspecific and more constrained instance.
Introduction
Logic synthesis is the process of turning an abstract circuit description into a concrete design in terms of logic gates. In the context of our riddle, the abstract description can be formalised as a set of goal functions which the circuit must realise:
Instead of thinking of a solution ourselves, we want to characterise the problem in terms of constraints whose solution can be interpreted as a solution to the riddle. To this end, we intend the constraints to describe a generic circuit that is parametrised by the functions that its gates realise, and the connections between these gates.
The following schematic illustrates one choice of connections (solid) from the many potential wirings (dashed) for an example with only one output $g_0$ and one gate $f_3$.
If $g_0$ were $x_0 \wedge x_1$, choosing the highlighted wiring and $f_3$ as AND would be a desirable logic synthesis result. Conceptually we want to guarantee something along these lines:
$$\tag{1}\forall x_0,x_1,x_2\ldotp g_0(x_0, x_1, x_2)=\mathit{circuit}(x_0,x_1,x_2)$$
where $\mathit{circuit}$ is defined by the choice of $f_3$ and the wiring. Here, $f_3$ and the wiring are the parameters which we, or a constraint solver, can tweak to establish the validity of $(1)$.
So what kind of wiring should we allow?
Considering the generic circuit with one gate, $g_0$ can only be connected to the inputs $x_0, x_1, x_2$ or the gate's output $x_3$.
Depending on which inputs $f_3$ is connected to, its output $x_3$ will be given by $f_3(x_0,x_1), f_3(x_0,x_2)$ or $f_3(x_1,x_2)$.
Note that it is sufficient to consider the input combinations $f_3(x_j, x_k)$ for $1\leq j < k < 3$ since $f_3$ is unconstrained (yet) and can represent any binary operator on Booleans.
In other words, if there were a solution with $x_3=f_3(x_2,x_1)$, we would also find it with $x_3=f_3(x_1, x_2)$ but the interpretation of $f_3$ mirrored
.
Allowing an arbitrary number of gates and arbitrary connections right from the start will result in an unnecessarily huge search space. Instead, we restrict ourselves to a fixed number of gates which we can increase incrementally if the current number of gates turns out to be insufficient to synthesise the goal function $g_0$. Without loss of generality, the inputs of a new gate $f_{n+1}$ may be connected to preceding gates (and inputs) $x_0,\dots,x_n$ but not the other way around, e.g. $x_4$ may not be an input of $f_3$. This was the adhoc approach my colleague and I figured should work, so I started implementing it.
SMTbased Logic Synthesis
Looking at the schematic from the introduction, characterising the logic synthesis problem boils down to:
 formulating how the outputs $g_i$ may be connected to the gates $x_0, \dots, x_n$, and
 formulating how the gates may be interconnected.
To denote that a gate $g_i$ is connected to $x_j$ we use a variable $g_{i,j}$. Similarly, we introduce variables $c_{i, j, k}$ to encode that $x_j$ is the first input of $f_i$, and $x_k$ the second one. With this in mind, reconsidering the wiring from our schematic, only $g_{0,3}$ and $c_{3,0,1}$ should be $\mathit{true}$.
For the simple case of $n=1$ inner gates, a circuit can be synthesised if (and only if) the following is satisfiable:
Here, the first part requires $g_0$ to be connected to at least one $x_i$, and the second part requires $f_3$ to be connected to some combination of inputs. In contrast to $(1)$, we now express the circuit's overall semantics $\mathit{circuit}(x_0, x_1, x_2)$ in terms of the functions realised by its gates. Increasing either the number of outputs or gates will merely add further conjuncts in the same vein.
However, this characterisation does not yet make use of the variables $g_{i,j}$ and $c_{i,j,k}$ to encode the chosen wiring. To bind the intended semantics to these variables, we let the variables imply the corresponding options and require at least one of them to be $\mathit{true}$.
This yields an equisatisfiable constraint:If there is an interpretation that satisfies $(2)$, then it can be extended to an interpretation that satisfies $(3)$ by picking appropriate values for $g_{i,j}$ and $c_{i,j,k}$ and vice versa.
Conceptually, that's all there is to characterising a generic logic synthesis problem in firstorder logic. However, to solve the introductory riddle we still have to restrict the functions $f_i$ to AND, OR and at most two NOTs.
Restricting the $f_i$ to AND, OR and NOT amounts to constraining each $f_i$ to these operators’ truth tables, i.e. also assert for each $f_i$:
Here, the first line is only satisfied by an AND, the second line is only satisfied by an OR, and the last line is only satisfied by a NOT on the gate's first or second input. This characterisation of NOT is needed since all of our $f_i$ have two parameters.
Having restricted the functions to the allowed gates, we can also limit the number of NOTs by means of cardinality constraints:
Implementation
Using the Python bindings of Z3, an implementation of this approach for arbitrary numbers of inputs, outputs and inner gates spans only few lines of code.
Functions over argument lists allow for an easy specification of the wanted outputs:


Providing the number of inputs and inner gates to consider, we can create lists of the corresponding variables $x_i$ and their uninterpreted functions $f_i:\mathbb{B}^2\rightarrow\mathbb{B}$ as follows:


The characterisation of possible output connections strongly follows the scheme shown in $(3)$. We create variables $g_{i,j}$ for the potential connection of $g_i$ and each $x_j$, and let them imply that $g_i(\mathit{inputs})=x_j$. It is also asserted that at least one $g_{i,j}$ for each $g_i$ must be $\mathit{true}$:


The characterisation of possible gate connections is very similar.
The enumeration of relevant input combinations can be achieved comfortably via itertools.combinations
:


Finally, the code for the riddlespecific additional constraints of $f_i$ closely resembles the constraints shown in the end of the previous section:


All that remains is simplifying these constraints and acquiring their SMTLIB representation – the common exchange format for SMT solvers:


The resulting characterisation works great for synthesis of smaller circuits, such as a full adder built from just ANDs, ORs and at most two NOTs:


Feel free to experiment with the implementation, feed the generated instances into SMT solvers, and interpret the found solutions before continuing with the SATbased approach. I've attached the full adder synthesis SMT instance to this post, so you don't have run the generator. The solution I get from Z3 describes the following circuit:
Unfortunately, the quantifiers, uninterpreted functions and cardinality constraints render the instance that characterises the introductory puzzle too difficult to be solved within several days. Therefore, in the next section, we reduce the characterisation to propositional logic, trading off the complexity of our constraints against a larger instance, and end up with a standard approach for SATbased logic synthesis. While the SMTbased synthesis of a full adder may take a few seconds, the corresponding SAT instance will be solvable in milliseconds.
SATbased Logic Synthesis
To make our problem approachable via SAT solving, we must reformulate the constraints to be free of quantifiers and uninterpreted functions. The cardinality constraints are less of a problem since (i) many SAT solvers support them, and (ii) Z3 can also reduce them to propositional logic for us.
Eliminating the Existential Quantifier
The first step of this reduction is understanding the $\exists$quantified gate outputs as functions of the $\forall$quantified circuit inputs. Clearly, the gates’ outputs depend on the current inputs. With this in mind, our example constraint $(3)$ can be rewritten as follows:
One detail that is easily overlooked is that the inner gates’ inputs are not guaranteed to be constants, such as $x_0,x_1$ and $x_2$, but may be function evaluations. For example, if we were to characterise a generic circuit with $n=2$ inner gates, the following clause would surface (among others): $$\tag{5} c_{4,0,3} \rightarrow x_4(x_0,x_1,x_2) = f_4(x_0,x_3(x_0,x_1,x_2))$$
Eliminating the Universal Quantifier
In next step we get rid of the $\forall$quantifier. Looking at how $\forall x$ is defined for a Boolean $x$: $$ \forall x\ldotp \varphi := \varphi[\mathit{true}/x] \wedge \varphi[\mathit{false}/x]$$ it is easy to see that we can eliminate one variable at a time by cloning the expression $\varphi$ and substituting $x$ by $\mathit{true}$ in the first instance and by $\mathit{false}$ in the second one. We effectively enumerate all the values the quantifier ranges over and conjunct the instantiated constraints.
By eliminating the $\forall$quantifier in $(4)$ like this, we end up with
where we again use $0$ and $1$ to denote $\mathit{false}$ and $\mathit{true}$, respectively. Note that we could as well have encoded the implications of $c_{3,0,1}$ in a single clause (like the implications of $g_{0,0}$). However, the illustrated encoding will make the upcoming elimination of uninterpreted functions more readable.
Although likely clear, I want to stress that if we had a more complex clause like $(5)$, it would be expanded into the following clauses:
Eliminating Uninterpreted Functions
The last step of the reduction is the elimination of the uninterpreted functions $f_i$ and the corresponding $x_i$. Since we're dealing with functions over Booleans, we can simply introduce a variable for each entry of a function's truth table, and encode the semantics in terms of these entries.
For example, a gate $f_4:\mathbb{B}^2\rightarrow \mathbb{B}$ can be encoded by an assignment to the four variables $$ f_{4,(0,0)}, f_{4,(0,1)}, f_{4,(1,0)}, f_{4,(1,1)} $$ each of which represents an entry of $f_4$'s truth table. Similarly, a function $x_i:\mathbb{B}^3\rightarrow \mathbb{B}$ will be blasted into $2^3$ variables $x_{i,(0,0,0)}, \dots, x_{i,(1,1,1)}$ to refer to the value of $x_i$ for different inputs.
Since the elimination of all uninterpreted functions from $(6)$ would take too much space, I will illustrate the approach on a single but generic clause: $$ c_{i,j,k} \rightarrow x_i(0,0,0) = f_i(x_j(0,0,0),x_k(0,0,0)) $$
If $x_j$ and $x_k$ are picked as the inputs of $f_i$, this constraint requires $f_i$ to relate the truth values of these inputs with the gate's output $x_i$, for a given circuit input $(0,0,0)$. To get rid of $f_i$ but express the same semantics with the new variables, we explicitly enumerate all $2^3$ possible combinations of input and output values of the gate, and require the corresponding $f_{i,(0,0)},\dots,f_{i,(1,1)}$ to be consistent with them:
Applying this transformation to the clauses from $(6)$ leaves us with a SAT instance that is equivalent to a standard formulation of SATbased logic synthesis.
Implementation
Since the implementation is mostly a refinement of the SMT instance generator, I will only touch on some aspects and refer to the implementation for details.
The biggest difference to the SMTbased characterisation is that we introduced variables $x_{i,(0,0,0)},\dots,x_{i,(1,1,1)}$ and $f_{i,(0,0),\dots,f_{i,(1,1)}}$ to refer to the values of $x_i$ and $f_i$ for every possible input. Accordingly, the implementation now uses lists of lists for indexing all the variants of $x_i$ and $f_i$:


Due to this indexing of variables, the restriction of $f_i$ has to be adapted slightly too. Instead of identifying a gate by its outputs for certain inputs, we now refer to each entry of the gate's truth table:


Besides the indexing, the implementation uses the very same reduction to SAT that has been sketched above, and maintains the general structure of the SMToriented implementation. What needs mention though is how to export the constraints in the DIMACS exchange format used by virtually all SAT solvers:


Z3 provides tactics that can be applied to a set of constraints.
By applying card2bv
, all occurring cardinality constraints will be reduced to propositional logic.
The subsequent tseitincnf
tactic brings the resulting constraints into conjunctive normal form (CNF) – in fact they almost are in CNF already.
The resulting constraints can then be output in the DIMACS format.
Although a SATbased characterisation is a lot larger than its SMTbased counterpart, it is less complex and is typically solved in ordersofmagnitude less time. Feel free to experiment with the implementation, or try to reconstruct the full adder circuit shown above from the generated SAT instance and the solution found by a SAT solver.
Still, the constraint that restricts the number of NOTs seems to make the SAT instance that characterises the introductory puzzle hard to solve. The next section proposes an additional assumption that is rather weak but sufficient to alleviate the combinatorial explosion, and make the constraints solvable in reasonable time.
Solving the Puzzle
The constraints that we used so far did not make any assumptions that could disregard potential solutions to the puzzle, but merely formalised the provided information. To make the combinatorial explosion more manageable, we will now incorporate an assumption that likely holds for the circuit, but may potentially disregard some solutions.
Our assumption is rather weak and concerns the connections of the outputs to the inner gates. We assume that if there is a solution, it likely can be formulated so that the outputs are connected to the very last gates of the circuit. In particular, each goal $g_i$ can certainly be computed independently, i.e. without referring to the value of an other output $g_j$. We can enforce these connections by extending our generic SATbased characterisation with:


With these additional constraints, it took an old i54690 CPU about 30min to solve the corresponding SAT instance with 19 inner gates. The synthesised circuit looks as follows:
Do Try This at Home!
Although the SATbased characterisation of logic synthesis turns out to be common in practice – especially without the artificial constraint on the number of gates – there is still room for improvement and experimentation. Here are some ideas that you might want to explore on your own (easiest first):
 Instead of relying on an external solver to solve the generated constraints, use the API to invoke the check programmatically.
 Does a solution to the riddle with less than 19 gates exist? Prove your hypothesis.
 Automate the interpretation of the solutions found by a solver as logic circuits, and plot them via DOT.
 Extend the characterisation to allow some composite gates. For example, I found that the expected solution has circuitry to decide whether more than one (or more than two) inputs are $\mathit{true}$. Requiring the synthesis to feature such blocks may speed up the synthesis of the puzzle's solution.
 Instead of characterising the circuit for a fixed number of gates, devise an incremental variant of SMTbased or SATbased synthesis which incorporates one additional gate at a time (and checks satisfiability). It should be advantageous to have the solver reuse information established during checks with fewer gates.
If you manage to solve the riddle without the domainspecific assumption, or have any ideas how to do this more efficiently with SAT/SMT solving, please let me know. It might also be possible to solve this with the logic synthesis tools mentioned in the paper that discusses the SATbased encoding we ended up with.