Circuits, Gates and Formulas

In Converting to CNF, we saw that logical connectives can be translated into clauses by treating them as equations.

Let's now look at how to do this in the Logical Modelling Tool. We'll use a domain to write down all the variables involved, and a parameterised atom active(n : var) which is true if that variable is true, and false otherwise.

Encoding NOT

We can encode Out = ¬ In as clauses like so, using the translation given in Conversion to CNF:

Clicking Run should give exactly the truth table for NOT.

Encoding AND

Similarly, we can encode AND as clauses, using the translation given in Conversion to CNF:

Clicking Run should give exactly the truth table for AND.

Encoding OR

And we can encode OR as clauses:

Clicking Run should give exactly the truth table for OR.

Encoding a Formula

Let's say we want to encode the formula Out = (¬In1 \/ In2) /\ (¬In2 \/ In1), and to find out all the values of In1 and In2 that make Out true.

To encode the formula as clauses, we break it down into individual components like so:

1. Out = X1 /\ X2

2. X1 = X3 \/ In2

3. X3 = ¬In1

4. X2 = X4 \/ In1

5. X4 = ¬In2

Now we can encode this formula using variables In1, In2, Out, X1, X2, X3, X4 and the logic gates defined above. We also assert that active(Out) is true to tell the solver that we want to find solutions when Out is true. Finally, we print out all solutions, but only to In1 and In2.

The results should say that Out is true exactly when In1 is equal to In2.

Extended Exercise: Adder Circuits

As we saw in when looking at patterns of constraints, it can be difficult to encode constraints like "exactly one of two", compared to "at most one". Constraints like "exactly two of three" or more get even harder, and the number of individual clauses we need can explode.

This exercise looks at a less elementary, but much more scalable approach to encode the 2-of-3 problem which generalises to any "n-of-m" problem.

The basic idea is simple: we will encode a circuit that adds up the three binary digits, and then checks that the answer is two. For this simple problem, this is overly complicated. However, for bigger numbers, or for problems where we wish to specify constraints like "at most 25 packages are installed", then encoding arithmetic as binary circuits is often a practical method.

Step 1: Encoding XOR

Exclusive-OR (XOR) has the following truth table:

Encode the XOR operation as a collection of constraints. The satisfying valuations of your constraints should exactly be the lines of the truth table (in some order, not necessarily the order in this table).

Hint: Try writing calculating how to represent the equation Output = Input1 XOR Input2 as clauses, as we did for the AND, OR, and NOT in the Tseytin transformation. You'll need to have a formula that expresses XOR in terms of &, | and ¬ before you can simplify. You should be able to do it with four clauses in xor.

define xor(x : node, y : node, z : node) {
  (~active(x) |  active(y) |  active(z)) &
  (~active(x) | ~active(y) | ~active(z)) &
  ( active(x) |  active(y) | ~active(z)) &
  ( active(x) | ~active(y) |  active(z))
}

Step 2: Encoding a Half-adder

A half adder circuit adds two binary digits Input1 and Input2 to produce a two bit output consisting of a Sum digit and a Carry digit. It can be constructed from an XOR and an AND:

As a truth table, a half adder acts as follows, where the first two columns are the input and the second two are the outputs.

Using your xor circuit and an and, write a definition that encodes a half adder circuit. The output from this problem should be exactly the truth table for the half-adder (again, in some order).

define half-adder(input1 : node,
                  input2 : node,
                  sum : node,
                  carry : node) {
  xor(sum, input1, input2) &
  and(carry, input1, input2)
}

Step 3: Encoding 2-of-3

Using two half adders and an OR to create a full adder, create a circuit with three inputs and two outputs where the two outputs are the sum of the three inputs as a two-digit binary number.

By adding additional constraints on the output nodes of the circuit, constrain the problem so that the solutions are all those for which 2 of the 3 inputs are true.