Boolean Expressions¶
Expressions are a very powerful and flexible way to represent Boolean functions. They are the central data type of PyEDA’s symbolic Boolean algebra engine. This chapter will explain how to construct and manipulate Boolean expressions.
The code examples in this chapter assume that you have already prepared your terminal by importing all interactive symbols from PyEDA:
>>> from pyeda.inter import *
Expression Constants¶
You can represent \(0\) and \(1\) as expressions:
>>> zero = expr(0)
>>> one = expr(1)
We will describe the expr
function in more detail later.
For now, let’s just focus on the representation of constant values.
All of the following conversions from \(0\) have the same effect:
>>> zeroA = expr(0)
>>> zeroB = expr(False)
>>> zeroC = expr("0")
All three “zero” objects are the same:
>>> zeroA == zeroB == zeroC
True
Similarly for \(1\):
>>> oneA = expr(1)
>>> oneB = expr(True)
>>> oneC = expr("1")
All three “one” objects are the same:
>>> oneA == oneB == oneC
True
However, these results might come as a surprise:
>>> expr(0) == 0
False
>>> expr(1) == True
False
PyEDA evaluates all zerolike and onelike objects,
and stores them internally using a modulelevel singleton in
pyeda.boolalg.expr
:
>>> type(expr(0))
pyeda.boolalg.expr._ExprZero
>>> type(expr(1))
pyeda.boolalg.expr._ExprOne
Once you have converted zero/one to expressions, they implement the full Boolean Function API.
For example, constants have an empty support set:
>>> one.support
frozenset()
Also, apparently zero is not satisfiable:
>>> zero.satisfy_one() is None
True
This fact might seem underwhelming, but it can have some neat applications. For example, here is a sneak peak of Shannon expansions:
>>> a, b = map(exprvar, 'ab')
>>> zero.expand([a, b], conj=True)
And(Or(a, b), Or(a, ~b), Or(~a, b), Or(~a, ~b))
>>> one.expand([a, b])
Or(And(~a, ~b), And(~a, b), And(a, ~b), And(a, b))
Expression Literals¶
A Boolean literal is defined as a variable or its complement. The expression variable and complement data types are the primitives of Boolean expressions.
Variables¶
To create expression variables, use the exprvar
function.
For example, let’s create a variable named \(a\),
and assign it to a Python object named a
:
>>> a = exprvar('a')
>>> type(a)
pyeda.boolalg.expr.ExprVariable
One efficient method for creating multiple variables is to use Python’s builtin
map
function:
>>> a, b, c = map(exprvar, 'abc')
The primary benefit of using the exprvar
function rather than a class
constructor is to ensure that variable instances are unique:
>>> a = exprvar('a')
>>> a_new = exprvar('a')
>>> id(a) == id(a_new)
True
You can name a variable pretty much anything you want, though we recommend standard identifiers:
>>> foo = exprvar('foo')
>>> holy_hand_grenade = exprvar('holy_hand_grenade')
By default, all variables go into a global namespace. You can assign a variable to a specific namespace by passing a tuple of strings as the first argument:
>>> a = exprvar('a')
>>> c_b_a = exprvar(('a', 'b', 'c'))
>>> a.names
('a', )
>>> c_b_a.names
('a', 'b', 'c')
Notice that the default representation of a variable will dot all the names together starting with the most significant index of the tuple on the left:
>>> str(c_b_a)
'c.b.a'
Since it is very common to deal with grouped variables, you may assign indices to variables as well. Each index is a new dimension.
To create a variable with a single index, use an integer argument:
>>> a42 = exprvar('a', 42)
>>> str(a42)
a[42]
To create a variable with multiple indices, use a tuple argument:
>>> a_1_2_3 = exprvar('a', (1, 2, 3))
>>> str(a_1_2_3)
a[1,2,3]
Finally, you can combine multiple namespaces and dimensions:
>>> c_b_a_1_2_3 = exprvar(('a', 'b', 'c'), (1, 2, 3))
>>> str(c_b_a_1_2_3)
c.b.a[1,2,3]
Note
The previous syntax is starting to get a bit cumbersome.
For a more powerful method of creating multidimensional arrays,
use the exprvars
function.
Complements¶
A complement is defined as the inverse of a variable. That is:
One way to create a complement from a preexisting variable is to simply
apply Python’s ~
unary negate operator.
For example, let’s create a variable and its complement:
>>> a = exprvar('a')
>>> ~a
~a
>>> type(~a)
pyeda.boolalg.expr.ExprComplement
All complements created from the same variable instance are not just identical, they all refer to the same object:
>>> id(~a) == id(~a)
True
Constructing Expressions¶
Expressions are defined recursively as being composed of primitives (constants, variables), and expressions joined by Boolean operators.
Now that we are familiar with all of PyEDA’s Boolean primitives, we will learn how to construct more interesting expressions.
From Constants, Variables, and Python Operators¶
PyEDA overloads Python’s ~
, 
, ^
, and &
operators with
NOT, OR, XOR, and AND, respectively.
Let’s jump in by creating a full adder:
>>> a, b, ci = map(exprvar, "a b ci".split())
>>> s = ~a & ~b & ci  ~a & b & ~ci  a & ~b & ~ci  a & b & ci
>>> co = a & b  a & ci  b & ci
Using XOR looks a lot nicer for the sum output:
>>> s = a ^ b ^ ci
You can use the expr2truthtable
function to do a quick check that the
sum logic is correct:
>>> expr2truthtable(s)
ci b a
0 0 0 : 0
0 0 1 : 1
0 1 0 : 1
0 1 1 : 0
1 0 0 : 1
1 0 1 : 0
1 1 0 : 0
1 1 1 : 1
Similarly for the carry out logic:
>>> expr2truthtable(co)
ci b a
0 0 0 : 0
0 0 1 : 0
0 1 0 : 0
0 1 1 : 1
1 0 0 : 0
1 0 1 : 1
1 1 0 : 1
1 1 1 : 1
From Factory Functions¶
Python does not have enough builtin operators to handle all interesting Boolean functions we can represent directly as an expression. Also, binary operators are limited to two operands at a time, whereas several Boolean operators are Nary (arbitrary many operands). This section will describe all the factory functions that can be used to create arbitrary Boolean expressions.
The general form of these functions is
OP(x [, x], simplify=True)
.
The function is an operator name, followed by one or more arguments,
followed by the simplify
parameter.
Some functions also have a conj
parameter,
which selects between conjunctive (conj=True
) and disjunctive
(conj=False
) formats.
One advantage of using these functions is that you do not need to create variable instances prior to passing them as arguments. You can just pass string identifiers, and PyEDA will automatically parse and convert them to variables.
For example, the following two statements are equivalent:
>>> Not('a[0]')
~a[0]
and:
>>> a0 = exprvar('a', 0)
>>> Not(a0)
~a[0]
Primary Operators¶
Since NOT, OR, and AND form a complete basis for a Boolean algebra, these three operators are primary.

Not
(x, simplify=True)¶ Return an expression that is the inverse of the input.

Or
(*xs, simplify=True)¶ Return an expression that evaluates to \(1\) if and only if any inputs are \(1\).

And
(*xs, simplify=True)¶ Return an expression that evaluates to \(1\) if and only if all inputs are \(1\).
Example of full adder logic using Not
, Or
, and And
:
>>> s = Or(And(Not('a'), Not('b'), 'ci'), And(Not('a'), 'b', Not('ci')), And('a', Not('b'), Not('ci')), And('a', 'b', 'ci'))
>>> co = Or(And('a', 'b'), And('a', 'ci'), And('b', 'ci'))
Secondary Operators¶
A secondary operator is a Boolean operator that can be natively represented as a PyEDA expression, but contains more information than the primary operators. That is, these expressions always increase in tree size when converted to primary operators.

Xor
(*xs, simplify=True)¶ Return an expression that evaluates to \(1\) if and only if the input parity is odd.
The word parity in this context refers to whether the number of ones in the input is even (divisible by two). For example, the input string “0101” has even parity (2 ones), and the input string “0001” has odd parity (1 ones).
The full adder circuit has a more dense representation when you
use the Xor
operator:
>>> s = Xor('a', 'b', 'ci')
>>> co = Or(And('a', 'b'), And('a', 'ci'), And('b', 'ci'))

Equal
(*xs, simplify=True)¶ Return an expression that evaluates to \(1\) if and only if all inputs are equivalent.

Implies
(p, q, simplify=True)¶ Return an expression that implements Boolean implication (\(p \implies q\)).
\(p\)  \(q\)  \(p \implies q\) 

0  0  1 
0  1  1 
1  0  0 
1  1  1 
Note that this truth table is equivalent to \(p \leq q\), but Boolean implication is by far the more common form due to its use in propositional logic.

ITE
(s, d1, d0, simplify=True)¶ Return an expression that implements the Boolean “if, then, else” operator. If \(s = 1\), then the output equals \(d_{0}\). Otherwise (\(s = 0\)), the output equals \(d_{1}\).
\(s\)  \(d_{1}\)  \(d_{0}\)  \(ite(s, d_{1}, d_{0})\) 

0  0  0  0 
0  0  1  1 
0  1  0  0 
0  1  1  1 
1  0  0  0 
1  0  1  0 
1  1  0  1 
1  1  1  1 
High Order Operators¶
A high order operator is a Boolean operator that can NOT be natively represented as a PyEDA expression. That is, these factory functions will always return expressions composed from primary and/or secondary operators.

Nor
(*xs, simplify=True)¶ Return an expression that evaluates to \(0\) if and only if any inputs are \(1\). The inverse of Or.

Nand
(*xs, simplify=True)¶ Return an expression that evaluates to \(0\) if an only if all inputs are \(1\). The inverse of And.

Xnor
(*xs, simplify=True)¶ Return an expression that evaluates to \(1\) if and only if the input parity is even.

Unequal
(*xs, simplify=True)¶ Return an expression that evaluates to \(1\) if and only if not all inputs are equivalent.

OneHot0
(*xs, simplify=True, conj=True)¶ Return an expression that evaluates to \(1\) if and only if the number of inputs equal to \(1\) is at most \(1\). That is, return true when at most one input is “hot”.

OneHot
(*xs, simplify=True, conj=True)¶ Return an expression that evaluates to \(1\) if and only if exactly one input is equal to \(1\). That is, return true when exactly one input is “hot”.

Majority
(*xs, simplify=True, conj=False)¶ Return an expression that evaluates to \(1\) if and only if the majority of inputs equal \(1\).
The full adder circuit has a much more dense representation when you
use both the Xor
and Majority
operators:
>>> s = Xor('a', 'b', 'ci')
>>> co = Majority('a', 'b', 'ci')

AchillesHeel
(*xs, simplify=True)¶ Return the Achille’s Heel function, defined as \(\prod_{i=0}^{N1}{(x_{i/2} + x_{i/2+1})}\).
The AchillesHeel
function has \(N\) literals in its CNF form,
but \(N/2 \times 2^{N/2}\) literals in its DNF form.
It is an interesting demonstration of tradeoffs when choosing an expression
representation.
For example:
>>> f = AchillesHeel('a', 'b', 'c', 'd', 'w', 'x', 'y', 'z')
>>> f
And(Or(a, b), Or(c, d), Or(w, x), Or(y, z))
>>> f.to_dnf()
Or(And(a, c, w, y), And(a, c, w, z), And(a, c, x, y), And(a, c, x, z), And(a, d, w, y), And(a, d, w, z), And(a, d, x, y), And(a, d, x, z), And(b, c, w, y), And(b, c, w, z), And(b, c, x, y), And(b, c, x, z), And(b, d, w, y), And(b, d, w, z), And(b, d, x, y), And(b, d, x, z))

Mux
(fs, sel, simplify=True)¶ Return an expression that multiplexes a sequence of input functions over a sequence of select functions.
For example:
>>> X = exprvars('x', 4)
>>> S = exprvars('s', 2)
>>> Mux(X, S)
Or(And(~s[0], ~s[1], x[0]), And(s[0], ~s[1], x[1]), And(~s[0], s[1], x[2]), And(s[0], s[1], x[3]))
From the expr
Function¶

expr
(obj, simplify=True)
The expr
function is very special.
It will attempt to convert the input argument to an Expression
object.
We have already seen how the expr
function converts a Python bool
input to a constant expression:
>>> expr(False)
0
Now let’s pass a str
as the input argument:
>>> expr('0')
0
If given an input string, the expr
function will attempt to parse the input
string and return an expression.
Examples of input expressions:
>>> expr("~a & b  ~c & d")
Or(And(~a, b), And(~c, d))
>>> expr("a  b ^ c & d")
Or(a, Xor(b, And(c, d)))
>>> expr("p => q")
Implies(p, q)
>>> expr("p <=> q")
Equal(p, q)
>>> expr("s ? d[1] : d[0]")
ITE(s, d[1], d[0])
>>> expr("Or(a, b, Not(c))")
Or(a, b, ~c)
>>> expr("Majority(a, b, c)")
Or(And(a, b), And(a, c), And(b, c))
Operator Precedence Table (lowest to highest):
Operator  Description 

s ? d1 : d0 
If Then Else 
=>
<=> 
Binary Implies, Binary Equal 
 
Binary OR 
^ 
Binary XOR 
& 
Binary AND 
~x 
Unary NOT 
(expr ...)
OP(expr ...) 
Parenthesis, Explicit operators 
The full list of valid operators accepted by the expression parser:
Or(...)
And(...)
Xor(...)
Xnor(...)
Equal(...)
Unequal(...)
Nor(...)
Nand(...)
OneHot0(...)
OneHot(...)
Majority(...)
AchillesHeel(...)
ITE(s, d1, d0)
Implies(p, q)
Not(a)
Expression Types¶
This section will cover the hierarchy of Boolean expression types.
Unsimplified¶
An unsimplified expression consists of the following components:
 Constants
 Expressions that can easily be converted to constants (eg \(x + x' = 1\))
 Literals
 Primary operators:
Not
,Or
,And
 Secondary operators
Also, an unsimplified expression does not automatically join adjacent, associative operators. For example, \(a + (b + c)\) is equivalent to \(a + b + c\). The depth of the unsimplified expression is two:
>>> f = Or('a', Or('b', 'c'), simplify=False)
>>> f.xs
(a, Or(b, c))
>>> f.depth
2
The depth of the simplified expression is one:
>>> g = f.simplify()
>>> g.xs
(b, a, c)
>>> g.depth
1
If the simplify=False
usage is too verbose,
you can use the Expression
subclasses directly to create unsimplified
expressions:
>>> ExprAnd(a, ~a)
And(~a, a)
>>> ExprOr(a, ExprOr(b, c))
Or(a, Or(b, c))
Notice that there are no unsimplified representations for:
 negated literals
 double negation
For example:
>>> ExprNot(a)
~a
>>> ExprNot(ExprNot(ExprOr(a, b)))
Or(a, b)
Simplifed¶
A simplified expression consists of the following components:
 Literals
 Primary operators:
Not
,Or
,And
 Secondary operators
Also, \(0\) and \(1\) are considered simplified by themselves.
That is, the act of simplifying an expression eliminates constants, and all subexpressions that can be easily converted to constants.
All expressions constructed using overloaded operatiors are automatically simplified:
>>> a  0
a
>>> a  1
1
>>> a  b & ~b
a
Unsimplified expressions are not very useful, so the factory functions also simplify by default:
>>> Or(a, And(b, ~b))
a
To simplify an expression, use the simplify
method:
>>> f = Or(a, 0, simplify=False)
>>> f
Or(0, a)
>>> g = f.simplify()
>>> g
a
You can check whether an expression is simplified using the simplified
attribute:
>>> f.simplified
False
>>> g.simplified
True
Negation Normal Form¶
An expression in Negation Normal Form (NNF) consists of the following components:
 Literals
 Primary operators:
Or
,And
That is, convert all secondary operators to primary operators,
and uses DeMorgan’s transform to eliminate Not
operators.
You can convert all secondary operators to NNF:
>>> Xor(a, b, c).to_nnf()
Or(And(~a, ~b, c), And(~a, b, ~c), And(a, ~b, ~c), And(a, b, c))
>>> Implies(p, q).to_nnf()
Or(~p, q)
>>> Equal(a, b, c).to_nnf()
Or(And(~a, ~b, ~c), And(a, b, c))
>>> ITE(s, a, b).to_nnf()
Or(And(b, Or(a, b, ~ci), Or(a, ~b, ci)), And(a, Or(And(~a, ~b, ci), And(~a, b, ~ci))))
Factoring also eliminates all Not
operators,
by using DeMorgan’s law:
>>> Not(a  b).to_nnf()
And(~a, ~b)
>>> Not(a & b).to_nnf()
Or(~a, ~b)
Normal Form¶
A normal form expression is an NNF expression with depth less than or equal to two.
That is, a normal form expression is a flattened NNF.
There are two types of normal forms:
 disjunctive normal form (SOP: sum of products)
 conjunctive normal form (POS: product of sums)
The preferred method for creating normal form expressions is to use the
to_dnf
and to_cnf
methods:
>>> f = Xor(a, Implies(b, c))
>>> f.to_dnf()
Or(And(~a, ~b), And(~a, c), And(a, b, ~c))
>>> f.to_cnf()
And(Or(~a, b), Or(~a, ~c), Or(a, ~b, c))
Canonical Normal Form¶
A canonical normal form expression is a normal form expression with the additional property that all terms in the expression have the same degree as the expression itself.
That is, a canonical normal form expression is a flattened, reduced NNF.
The preferred method for creating canonical normal form expressions is to use
the to_cdnf
and to_ccnf
methods.
Using the same function from the previous section as an example:
>>> f = Xor(a, Implies(b, c))
>>> f.to_cdnf()
Or(And(~a, ~b, ~c), And(~a, ~b, c), And(~a, b, c), And(a, b, ~c))
>>> f.to_ccnf()
And(Or(a, ~b, c), Or(~a, b, c), Or(~a, b, ~c), Or(~a, ~b, ~c))
Depth¶
Expressions are a type of tree data structure. The depth of a tree is defined recursively:
 A leaf node (constant or literal) has zero depth.
 A branch node (operator) has depth equal to the maximum depth of its children (arguments) plus one.
You can think of the depth as the maximum number of operators between the expression’s inputs to its output.
For example:
>>> a.depth
0
>>> (a & b).depth
1
>>> Xor(a, Implies(b, c)).depth
2
Satisfiability¶
Expressions have smart support for Boolean satisfiability.
They inherit both the satisfy_one
and satisfy_all
methods from the
Function
interface.
For example:
>>> f = Xor('a', Implies('b', 'c'))
>>> f.satisfy_one()
{a: 0, b: 0}
>>> list(f.satisfy_all())
[{a: 0, b: 0}, {a: 0, b: 1, c: 1}, {a: 1, b: 1, c: 0}]
By default, Boolean expressions use a very naive “backtracking” algorithm to solve for satisfying input points. Since SAT is an NPcomplete algorithm, you should always use care when preparing your inputs.
A conjunctive normal form expression will automatically use the PicoSAT C extension. This is an industrialstrength SAT solver, and can be used to solve very nontrivial problems.
>>> g = f.to_cnf()
>>> g.satisfy_one()
{a: 0, b: 0, c: 1}
>>> list(g.satisfy_all())
[{a: 0, b: 1, c: 1},
{a: 0, b: 0, c: 0},
{a: 0, b: 0, c: 1},
{a: 1, b: 1, c: 0}]
Note
Future versions of PyEDA might support additional C/C++ extensions for SAT solving. This is an active area of research, and no single solver is ideal for all cases.
Assumptions¶
A common pattern in SATsolving is to setup a large database of clauses, and attempt to solve the CNF several times with different simplifying assumptions. This is equivalent to adding unit clauses to the database, which can be easily eliminated by boolean constraint propagation.
The Expression
data type supports applying assumptions using the with
statement.
Here is an example of creating a nested context of literals that assumes
a=1
and b=0
:
>>> f = Xor(a, b, c)
>>> with a, ~b:
... print(f.satisfy_one())
{a: 1, b: 0, c: 0}
There are four satisfying solutions to this function, but the return value will always correspond to the input assumptions.
And
terms of literals (clauses) may also be used as assumptions:
>>> with a & ~b:
... print(f.satisfy_one())
{a: 1, b: 0, c: 0}
Note that it is an error to assume conflicting values for a literal:
>>> with a, ~a:
... print(f.satisfy_one())
ValueError: conflicting constraints: a, ~a
PicoSAT Script¶
Starting with version 0.23.0
, PyEDA includes a script that implements
some of the functionality of the PicoSAT commandline utility.
$ picosat h
usage: picosat [h] [version] [n] [a LIT] [v] [i {0,1,2,3}] [P LIMIT]
[l LIMIT] [all]
[file]
PicoSAT solver
positional arguments:
file CNF input file (default: stdin)
optional arguments:
h, help show this help message and exit
version print version and exit
...
Here is an example of a basic SAT problem encoded using the wellknown DIMACS CNF format. See http://www.satcompetition.org/ for details on expected inputs and outputs. The function is a onehot function on four input variables.
$ cat onehot4.cnf
c Comments start with a 'c' character
c The problem 'p' line is followed by clauses
p cnf 4 7
1 2 3 4 0
4 3 0
4 2 0
4 1 0
3 2 0
3 1 0
2 1 0
To get one satisfying solution:
$ picosat onehot4.cnf
s SATISFIABLE
v 1 2 3 4 0
To get all satisfying solutions:
$ picosat all onehot4.cnf
s SATISFIABLE
v 1 2 3 4 0
s SATISFIABLE
v 1 2 3 4 0
s SATISFIABLE
v 1 2 3 4 0
s SATISFIABLE
v 1 2 3 4 0
s SOLUTIONS 4
You can also constrain the solver with one or more assumptions:
$ picosat a 1 a 2 onehot4.cnf
s SATISFIABLE
v 1 2 3 4 0
$ picosat a 1 a 2 onehot4.cnf
s UNSATISFIABLE
Tseitin’s Encoding¶
To take advantage of the PicoSAT solver, you need an expression that is in conjunctive normal form. Some expressions (especially Xor) have exponentially large size when you expand them to a CNF.
One way to work around this limitation is to use Tseitin’s encoding.
To convert an expression to Tseitin’s encoding, use the tseitin
method:
>>> f = Xor('a', Implies('b', 'c'))
>>> tf = f.tseitin()
>>> tf
And(Or(a, ~aux[0]), Or(~a, aux[0], ~b, c), Or(~a, ~aux[2]), Or(a, ~aux[1], aux[2]), Or(aux[0], aux[2]), Or(~aux[0], b), Or(~aux[0], ~c), Or(aux[1], ~aux[2]), Or(aux[1], b), Or(aux[1], ~c), Or(~aux[1], ~b, c))
As you can see, Tseitin’s encoding introduces several “auxiliary” variables into the expression.
You can change the name of the auxiliary variable by using the auxvarname
parameter:
>>> f = Xor('a', Implies('b', 'c'))
>>> f.tseitin(auxvarname='z')
And(Or(a, ~z[0]), Or(~a, ~b, c, z[0]), Or(~a, ~z[2]), Or(a, ~z[1], z[2]), Or(b, z[1]), Or(~b, c, ~z[1]), Or(b, ~z[0]), Or(~c, ~z[0]), Or(~c, z[1]), Or(z[0], z[2]), Or(z[1], ~z[2]))
You will see the auxiliary variables in the satisfying points:
>>> tf.satisfy_one()
{a: 0, aux[0]: 0, aux[1]: 1, aux[2]: 1, b: 0, c: 1}
>>> list(tf.satisfy_all())
[{a: 1, aux[0]: 0, aux[1]: 0, aux[2]: 1, b: 1, c: 0},
{a: 0, aux[0]: 1, aux[1]: 1, aux[2]: 0, b: 1, c: 1},
{a: 0, aux[0]: 1, aux[1]: 1, aux[2]: 0, b: 0, c: 0},
{a: 0, aux[0]: 1, aux[1]: 1, aux[2]: 0, b: 0, c: 1}]
Just filter them out to get the answer you’re looking for:
>>> [{v: val for v, val in point.items() if v.name != 'aux'} for point in tf.satisfy_all()]
[{a: 1, b: 1, c: 0},
{a: 0, b: 1, c: 1},
{a: 0, b: 0, c: 0},
{a: 0, b: 0, c: 1}]
Formal Equivalence¶
Two Boolean expressions \(f\) and \(g\) are formally equivalent if \(f \oplus g\) is not satisfiable.
Boolean expressions have an equivalent
method that implements this basic
functionality.
It uses the naive backtracking SAT,
because it is difficult to determine whether any particular expression can
be converted efficiently to a CNF.
Let’s test whether bit 6 of a ripple carry adder is equivalent to bit 6 of a Kogge Stone adder:
>>> from pyeda.logic.addition import ripple_carry_add, kogge_stone_add
>>> A = exprvars('a', 16)
>>> B = exprvars('b', 16)
>>> S1, C1 = ripple_carry_add(A, B)
>>> S2, C2 = kogge_stone_add(A, B)
>>> S1[6].equivalent(S2[6])
True
Note that this is the same as the following:
>>> Xor(S1[6], S2[6]).satisfy_one() is None
True