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 SAT-based logic synthesis to a problem-specific 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: $$ \begin{aligned} g_0(x_0,x_1,x_2) &=\neg x_0\\ g_1(x_0,x_1,x_2)&=\neg x_1\\ g_2(x_0,x_1,x_2)&=\neg x_2 \end{aligned} $$ where $x_0,x_1,x_2$ are the circuit’s Boolean inputs.

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$.

Generic 1-gate circuit

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 ad-hoc approach my colleague and I figured should work, so I started implementing it.

SMT-based Logic Synthesis

Looking at the schematic from the introduction, characterising the logic synthesis problem boils down to:

  1. formulating how the outputs $g_i$ may be connected to the gates $x_0, \dots, x_n$, and
  2. 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}$.

Connection variables

For the simple case of $n=1$ inner gates, a circuit can be synthesised if (and only if) the following is satisfiable: $$ \tag{2} \begin{aligned} \forall x_0,x_1,x_2~ \exists x_3\ldotp &~ (g_0(x_0,x_1,x_2) = x_0\\ \vee &~ g_0(x_0,x_1,x_2)= x_1\\ \vee &~ g_0(x_0,x_1,x_2)= x_2\\ \vee &~ \textcolor{a6e22e}{g_0}(x_0,x_1,x_2)= \textcolor{a6e22e}{x_3})\\ \wedge &~ (x_3=\textcolor{f92672}{f_3(x_0,x_1)}\\ \vee &~ x_3 = f_3(x_0,x_2)\\ \vee &~ x_3 = f_3(x_1,x_2)) \end{aligned} $$

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:

$$ \tag{3} \begin{aligned} \forall x_0,x_1,x_2~ \exists x_3\ldotp &~ (g_{0,0}\rightarrow g_0(x_0,x_1,x_2) = x_0)\\ \wedge &~ (g_{0,1}\rightarrow g_0(x_0,x_1,x_2)= x_1)\\ \wedge &~ (g_{0,2}\rightarrow g_0(x_0,x_1,x_2)= x_2)\\ \wedge &~ (\textcolor{a6e22e}{g_{0,3}}\rightarrow g_0(x_0,x_1,x_2)= x_3)\\ \wedge &~ (g_{0,0} \vee g_{0,1} \vee g_{0,2} \vee \textcolor{a6e22e}{g_{0,3}})\\ \wedge &~ (\textcolor{f92672}{c_{3,0,1}}\rightarrow x_3 = f_3(x_0,x_1))\\ \wedge &~ (c_{3,0,2}\rightarrow x_3 = f_3(x_0,x_2))\\ \wedge &~ (c_{3,1,2}\rightarrow x_3 = f_3(x_1,x_2))\\ \wedge &~ (\textcolor{f92672}{c_{3,0,1}} \vee c_{3,0,2} \vee c_{3,1,2}) \end{aligned} $$

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 first-order 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$ that $$ \begin{aligned} &(\neg f_i(0,0) \wedge \neg f_i(0, 1) \wedge \neg f_i(1,0) \wedge f_i(1, 1))\\ \vee~ & (\neg f_i(0,0) \wedge f_i(0, 1) \wedge f_i(1,0) \wedge f_i(1, 1))\\ \vee~ & (f_i(0,0) \wedge \neg f_i(0, 1) = f_i(1,0) \wedge \neg f_i(1, 1))\\ \end{aligned} $$

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: $$ \begin{aligned} & (f_3(0,0) \wedge \neg f_3(0, 1) = f_3(1,0) \wedge \neg f_3(1, 1))\\ +~& (f_4(0,0) \wedge \neg f_4(0, 1) = f_4(1,0) \wedge \neg f_4(1, 1))\\ &~ \vdots\\ +~& (f_n(0,0) \wedge \neg f_n(0, 1) = f_n(1,0) \wedge \neg f_n(1, 1))\\ \leq~& 2 \end{aligned} $$ essentially constraining how many $f_i$ may be interpreted as NOTs.

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:

62
63
64
65
66

# Original puzzle (possible with 19 gates)
g0 = lambda inputs: Not(inputs[0])
g1 = lambda inputs: Not(inputs[1])
g2 = lambda inputs: Not(inputs[2])
outputs = [g0, g1, g2]
gen_smt2.py

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:

41
42
43
44
45
46

# Create variables (and values for inputs) for each x_i
x = [Bool("x{:d}".format(gate_idx)) for gate_idx in range(num_inputs + num_inner_gates)]

# Create functions f:B^2-->B realised by the inner gates
f_sig = [BoolSort()]*3
f = [Function("f{:d}".format(gate_idx), f_sig) for gate_idx in range(num_inputs, len(x))]
gen_smt2.py

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}$:

 4
 5
 6
 7
 8
 9
10
11
12
13

def output_connections(num_inputs, x, outputs):
    asserts = []
    for output_idx in range(len(outputs)):
        conn_vars = []
        for gate_idx in range(len(x)):
            conn_var = Bool("g_{:d}_{:d}".format(output_idx, gate_idx))
            conn_vars.append(conn_var)
            asserts.append(Implies(conn_var, outputs[output_idx](x[:num_inputs]) == x[gate_idx]))
        asserts.append(Or(conn_vars))
    return asserts
gen_smt2.py

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

15
16
17
18
19
20
21
22
23
24
25

def gate_connections(num_inputs, x, f):
    asserts = []
    for gate_idx in range(num_inputs, len(x)):
        print("Encoding gate {}".format(gate_idx))
        conn_vars = []
        for in1_idx, in2_idx in combinations(range(gate_idx), 2):
            conn_var = Bool("c_{:d}_{:d}_{:d}".format(gate_idx, in1_idx, in2_idx))
            conn_vars.append(conn_var)
            asserts.append(Implies(conn_var, x[gate_idx] == f[gate_idx - num_inputs](x[in1_idx], x[in2_idx])))
        asserts.append(Or(conn_vars))
    return asserts
gen_smt2.py

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

27
28
29
30
31
32
33
34
35
36
37
38

def f_constraints(f):
    asserts = []
    is_and = lambda gate: And(Not(gate(False, False)), Not(gate(False, True)), Not(gate(True, False)), gate(True, True))
    is_or = lambda gate: And(Not(gate(False, False)), gate(False, True), gate(True, False), gate(True, True))
    is_not = lambda gate: And(gate(False, False), gate(False, True) != gate(True, False), Not(gate(True, True)))

    for gate in f:
        gate_filters = [is_and(gate), is_or(gate), is_not(gate)]
        asserts.append(Or(gate_filters))
    if len(f) > 0:
        asserts.append(AtMost([is_not(gate) for gate in f] + [2]))
    return asserts
gen_smt2.py

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

49
50
51
52
53
54

s = Solver()
constraints = output_connections(num_inputs, x, outputs) + gate_connections(num_inputs, x, f) + f_constraints(f)
simplified = And([simplify(assrt) for assrt in constraints])
quantified = ForAll(x[:num_inputs], Exists(x[num_inputs:], simplified) if num_inner_gates > 0 else simplified)
s.add(quantified)
return s.to_smt2() + "(get-model)\n"
gen_smt2.py

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:

58
59
60
61

# Full adder example (impossible with 8 restricted gates; possible with 9)
sum = lambda inputs: Xor(Xor(inputs[0], inputs[1]), inputs[2])
carry = lambda inputs: Or(And(inputs[0], inputs[1]), And(Xor(inputs[0], inputs[1]), inputs[2]))
outputs = [sum, carry]
gen_smt2.py

Feel free to experiment with the implementation, feed the generated instances into SMT solvers, and interpret the found solutions before continuing with the SAT-based 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:

Visualisation of synthesised full adder

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 SAT-based logic synthesis. While the SMT-based synthesis of a full adder may take a few seconds, the corresponding SAT instance will be solvable in milliseconds.

SAT-based 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:

$$ \tag{4} \begin{aligned} \forall x_0,x_1,x_2\ldotp &~ (g_{0,0}\rightarrow g_0(x_0,x_1,x_2) = x_0)\\ \wedge &~ (g_{0,1}\rightarrow g_0(x_0,x_1,x_2)= x_1)\\ \wedge &~ (g_{0,2}\rightarrow g_0(x_0,x_1,x_2)= x_2)\\ \wedge &~ (g_{0,3}\rightarrow g_0(x_0,x_1,x_2)= x_3(x_0,x_1,x_2))\\ \wedge &~ (g_{0,0} \vee g_{0,1} \vee g_{0,2} \vee g_{0,3})\\ \wedge &~ (c_{3,0,1}\rightarrow x_3(x_0,x_1,x_2) = f_3(x_0,x_1))\\ \wedge &~ (c_{3,0,2}\rightarrow x_3(x_0,x_1,x_2) = f_3(x_0,x_2))\\ \wedge &~ (c_{3,1,2}\rightarrow x_3(x_0,x_1,x_2) = f_3(x_1,x_2))\\ \wedge &~ (c_{3,0,1} \vee c_{3,0,2} \vee c_{3,1,2}) \end{aligned} $$

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 $$ \tag{6} \begin{aligned} & \begin{aligned} (g_{0,0} \rightarrow&~ g_0(0,0,0) = 0)\\ \wedge&~ g_0(0,0,1) = 0)\\ \wedge&~ g_0(0,1,0) = 0)\\ \wedge&~ g_0(0,1,1) = 0)\\ \wedge&~ g_0(1,0,0) = 1)\\ \wedge&~ g_0(1,0,1) = 1)\\ \wedge&~ g_0(1,1,0) = 1)\\ \wedge&~ g_0(1,1,1) = 1))\\ \end{aligned}\\ \wedge~ & (g_{0,1} \rightarrow~ \dots )\\ \wedge~ & (g_{0,2} \rightarrow~ \dots )\\ \wedge~ & (g_{1,2} \rightarrow~ \dots )\\ \wedge~ & (g_{0,0} \vee g_{0,1} \vee g_{0,2} \vee g_{0,3})\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(0,0,0) = f_3(0,0))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(0,0,1) = f_3(0,0))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(0,1,0) = f_3(0,1))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(0,1,1) = f_3(0,1))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(1,0,0) = f_3(1,0))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(1,0,1) = f_3(1,0))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(1,1,0) = f_3(1,1))\\ \wedge~ & (c_{3,0,1} \rightarrow~ x_3(1,1,1) = f_3(1,1))\\ \wedge~ & (c_{3,0,2} \rightarrow~ \dots )\\ \wedge~ & (c_{3,1,2} \rightarrow~ \dots )\\ \wedge~ &(c_{3,0,1} \vee c_{3,0,2} \vee c_{3,1,2}) \end{aligned} $$ 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:

$$ \begin{aligned} &~(c_{4,0,3} \rightarrow x_4(0,0,0) = f_4(0,x_3(0,0,0)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(0,0,1) = f_4(0,x_3(0,0,1)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(0,1,0) = f_4(0,x_3(0,1,0)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(0,1,1) = f_4(0,x_3(0,1,1)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(1,0,0) = f_4(1,x_3(1,0,0)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(1,0,1) = f_4(1,x_3(1,0,1)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(1,1,0) = f_4(1,x_3(1,1,0)))\\ \wedge&~ (c_{4,0,3} \rightarrow x_4(1,1,1) = f_4(1,x_3(1,1,1))) \end{aligned} $$

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:

$$ \begin{aligned} &~ (c_{i,j,k} \wedge \neg x_{i,(0,0,0)} \wedge \neg x_{j,(0,0,0)} \wedge \neg x_{k,(0,0,0)} \rightarrow \neg f_{4,(0,0)})\\ \wedge &~ (c_{i,j,k} \wedge \neg x_{i,(0,0,0)} \wedge \neg x_{j,(0,0,0)} \wedge x_{k,(0,0,0)} \rightarrow \neg f_{4,(0,1)})\\ \wedge &~ (c_{i,j,k} \wedge \neg x_{i,(0,0,0)} \wedge x_{j,(0,0,0)} \wedge \neg x_{k,(0,0,0)} \rightarrow \neg f_{4,(1,0)})\\ \wedge &~ (c_{i,j,k} \wedge \neg x_{i,(0,0,0)} \wedge x_{j,(0,0,0)} \wedge x_{k,(0,0,0)} \rightarrow \neg f_{4,(1,1)})\\ \wedge &~ (c_{i,j,k} \wedge x_{i,(0,0,0)} \wedge \neg x_{j,(0,0,0)} \wedge \neg x_{k,(0,0,0)} \rightarrow f_{4,(0,0)})\\ \wedge &~ (c_{i,j,k} \wedge x_{i,(0,0,0)} \wedge \neg x_{j,(0,0,0)} \wedge x_{k,(0,0,0)} \rightarrow f_{4,(0,1)})\\ \wedge &~ (c_{i,j,k} \wedge x_{i,(0,0,0)} \wedge x_{j,(0,0,0)} \wedge \neg x_{k,(0,0,0)} \rightarrow f_{4,(1,0)})\\ \wedge &~ (c_{i,j,k} \wedge x_{i,(0,0,0)} \wedge x_{j,(0,0,0)} \wedge x_{k,(0,0,0)} \rightarrow f_{4,(1,1)})\\ \end{aligned} $$

Applying this transformation to the clauses from $(6)$ leaves us with a SAT instance that is equivalent to a standard formulation of SAT-based 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 SMT-based 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$:

53
54
55
56
57
58
59
60
61
62
63

# Create variables (and values for inputs) for each x_i, given concrete inputs
x = [[Bool("x{:d}{}".format(gate_idx, val)) for val in product(range(2), repeat=num_inputs)]
     for gate_idx in range(num_inputs + num_inner_gates)]
# Replace variables for inputs by concrete values
for input_idx in range(num_inputs):
    for idx, bits in enumerate(product(range(2), repeat=num_inputs)):
        x[input_idx][idx] = BoolVal(bits[input_idx])

# Create functions f:B^2-->B realised by the inner gates
f = [[Bool("f{:d}{}".format(gate_idx, val)) for val in product(range(2), repeat=2)]
     for gate_idx in range(num_inputs, len(x))]
gen_sat.py

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:

40
41
42

is_and = lambda gate: And(Not(gate[0]), Not(gate[1]), Not(gate[2]), gate[3])
is_or = lambda gate: And(Not(gate[0]), gate[1], gate[2], gate[3])
is_not = lambda gate: And(gate[0], Not(gate[1]) == gate[2], Not(gate[3]))
gen_sat.py

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

66
67
68
69
70
71
72
73
74
75

goal = Goal()
for assrt in output_connections(num_inputs, x, outputs) + gate_connections(num_inputs, x, f) + f_constraints(f):
    goal.add(simplify(assrt))

# Reduce cardinality constraints; transform to CNF
to_cnf = Then(Tactic("card2bv"), Tactic("tseitin-cnf"))
subgoals = to_cnf(goal)
assert len(subgoals) == 1, "Tactic should have resulted in a single goal"
assert not subgoals[0].inconsistent(), "Found to be UNSAT during pre-processing"
return subgoals[0].dimacs() + "\n"
gen_sat.py

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 tseitin-cnf 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 SAT-based characterisation is a lot larger than its SMT-based counterpart, it is less complex and is typically solved in orders-of-magnitude 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 SAT-based characterisation with:

16
17
18

# Connect outputs to last gates
if output_idx == len(x) - 1 - gate_idx:
    asserts.append(conn_var)
gen_puzzle.py

With these additional constraints, it took an old i5-4690 CPU about 30min to solve the corresponding SAT instance with 19 inner gates. The synthesised circuit looks as follows:

Solution to puzzle

Since we only allow gates with fan-in 2, here, the NOT2 denotes a NOT on the second input.

Do Try This at Home!

Although the SAT-based 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 SMT-based or SAT-based 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 domain-specific 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 SAT-based encoding we ended up with.

full_adder.cnf full_adder.smt2 puzzle.cnf full_adder.log gen_puzzle.py gen_sat.py gen_smt2.py puzzle.log

Related Posts

Solving the "Seven Segment Search" Puzzle with Z3

This week I stumbled upon someone wondering whether the second part of the recent Advent of Code puzzle “Seven Segment Search” can be expressed as a constraint satisfaction problem. As attested by the replies: yes, it can. However, I think the question deserves a more extensive discussion than just a few comments in a thread. This post tries to provide a more instructive answer and raise awareness for the tradeoffs or solver misuses some solutions put up with.

I assume that the reader is familiar with mathematical notation and

  • just struggles to express the posed problem in a formal, declarative way, or
  • is interested in seeing how the SMT solver Z3 can be used to express and solve the problem in several logics. It takes only few steps to get from a quantifier-laden high-level formulation to what is effectively propositional logic.
» Read more

Generating Crosswords via SAT/SMT

Recently I got interested in designing personalised crosswords as a way to spice up photo book presents. This made me realise how hard generating high-quality crosswords actually is. Trying to create a crossword from a set of words – or a subset thereof – I checked out several tools but found all of them to be based on heuristics and yield rather sparse crosswords.

In line with the general theme of my previous posts, this one illustrates how we can leverage SAT solving to solve this problem. In contrast to related approaches, which assume a fixed grid structure and search for fitting words, we consider word placement as part of the problem and eventually end up with an integrated solution to generating crosswords of adjustable quality.

» Read more