Python EDA Documentation¶

Linux Notes¶

If you are using the Linux system distribution of pip, most likely pip will be part of Python-2.x, which won’t work. It’s safer to always use pip3.

You will probably need to install the Python3 “development” package to get Python’s headers and libraries. For Debian derivatives (eg Ubuntu), run sudo apt-get install python3-dev. On RedHat derivatives, run sudo yum install python3-devel.

Windows Notes¶

I highly recommend Christophe Gohlke’s pythonlibs page for installing PyEDA on Windows.

If you are using a Windows wheel distribution, you may need to install the [Visual Studio 2012 Redistributable](http://www.microsoft.com/en-us/download/details.aspx?id=30679).

Complement Operator¶

The complement operator is a unary operator, which means it acts on a single Boolean input: \(x\). The Boolean complement of \(x\) is usually written as \(x'\), \(\overline{x}\), or \(\lnot x\).

The output of the Boolean complement is defined by:

Sum Operator¶

The sum (or disjunction) operator is a binary operator, which means it acts on two Boolean inputs: \((x, y)\). The Boolean sum of \(x\) and \(y\) is usually written as \(x + y\), or \(x \vee y\).

The output of the Boolean sum is defined by:

This looks familiar so far except for the \(1 + 1 = 1\) part. The Boolean sum operator is also called OR because the output of \(x\) or \(y\) equals 1 if and only if \(x = 1\), or \(y = 1\), or both.

Product Operator¶

The product (or conjunction) operator is also a binary operator. The Boolean product of \(x\) and \(y\) is usually written as \(x \cdot y\), or \(x \wedge y\).

The output of the Boolean product is defined by:

As you can see, the product operator looks exactly like normal multiplication. The Boolean product is also called AND because the output of \(x\) and \(y\) equals 1 if and only if both \(x = 1\), and \(y = 1\).

Other Binary Operators¶

For reference, here is a table of all binary Boolean operators:

Some additional notes:

• \(f \downarrow g\) is the binary NOR (not or) operator.
• \(f \uparrow g\) is the binary NAND (not and) operator.
• \(f \leq g\) is commonly written using the binary implication operator \(f \implies g\).
• \(f = g\) is commonly written using either the binary equivalence operator \(f \iff g\), or the binary XNOR (exclusive nor) operator \(f \odot g\).
• \(f \ne g\) is commonly written using the binary XOR (exclusive or) operator \(f \oplus g\).

Additional Perspective¶

You are probably thinking this is all very nice, but what can you possibly do with an algebra that only concerns itself with 0, 1, NOT, OR, and AND?

In 1937, Claude Shannon realized that electronic circuits have two-value switches that can be combined into networks capable of solving any logical or numeric relationship. A transistor is nothing but an electrical switch. Similar to a light bulb, it has two states: off (0), and on (1). Wiring transistors together in serial imitates the AND operator, and wiring them together in parallel imitates the OR operator. If you wire a few thousand transistors together in interesting ways, you can build a computer.

Creating Variable Instances¶

Let’s create a few Boolean expression variables using the exprvar method:

>>> a, b, c, d = map(exprvar, 'abcd')
>>> a.name
a
>>> b.name
b

By default, all variables go into a global namespace. Also, all variable instances are singletons. That is, only one variable is allowed to exist per name. Verify this fact with the following:

>>> a = exprvar('a')
>>> _a = exprvar('a')
>>> id(a) == id(_a)
True

Indexing Variables¶

“There are only two hard things in Computer Science: cache invalidation and naming things.”

—Tim Bray

Consider the coin-flipping example from before. But this time, instead of flipping one coin, we want to flip a hundred coins. You could start naming your variables by assigning the first flip to \(x\), followed by \(y\), and so on. But there are only twenty-six letters in the English alphabet, so unless we start resorting to other alphabets, we will hit some limitations with this system very quickly.

For cases like these, it is convenient to give variables an index. Then, you can name the variable for the first coin flip \(x[0]\), followed by \(x[1]\), \(x[2]\), and so on.

Here is how to give variables indices using the exprvar function:

>>> x_0 = exprvar('x', 0)
>>> x_1 = exprvar('x', 1)
>>> x_0, x_1
(x[0], x[1])

You can even give variables multiple indices by using a tuple:

>>> x_0_1_2_3 = exprvar('x', (0, 1, 2 ,3))
>>> x_0_1_2_3
x[0,1,2,3]

Assigning individual variables names like this is a bit cumbersome. It is much easier to just use the exprvars factory function:

>>> X = exprvars('x', 8)
>>> X
[x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7]]
>>> X[3]
x[3]
>>> X[2:5]
[x[2], x[3], x[4]]
>>> X[:5]
[x[0], x[1], x[2], x[3], x[4]]
>>> X[5:]
[x[5], x[6], x[7]]
>>> X[-1]
x[7]

Similary for multi-dimensional bit vectors:

>>> X = exprvars('x', 4, 4)
>>> X
farray([[x[0,0], x[0,1], x[0,2], x[0,3]],
        [x[1,0], x[1,1], x[1,2], x[1,3]],
        [x[2,0], x[2,1], x[2,2], x[2,3]],
        [x[3,0], x[3,1], x[3,2], x[3,3]]])
>>> X[2]
farray([x[2,0], x[2,1], x[2,2], x[2,3]])
>>> X[2,2]
x[2,2]
>>> X[1:3]
farray([[x[1,0], x[1,1], x[1,2], x[1,3]],
        [x[2,0], x[2,1], x[2,2], x[2,3]]])
>>> X[1:3,2]
farray([x[1,2], x[2,2]])
>>> X[2,1:3]
farray([x[2,1], x[2,2]])
>>> X[-1,-1]
x[3,3]

Boolean Variables¶

In order to easily support algebraic operations on Boolean functions, each function representation has a corresponding variable representation. For example, truth table variables are instances of TruthTableVariable, and expression variables are instances of ExpressionVariable, both of which inherit from Variable.

class pyeda.boolalg.boolfunc.Variable(names, indices)[source]

Base class for a symbolic Boolean variable.

A Boolean variable is an abstract numerical quantity that may assume any value in the set \(B = \{0, 1\}\).

Note

Do NOT instantiate a Variable directly. Instead, use one of the concrete implementations: pyeda.boolalg.bdd.bddvar() pyeda.boolalg.expr.exprvar(), pyeda.boolalg.table.ttvar().

A variable is defined by one or more names, and zero or more indices. Multiple names establish hierarchical namespaces, and multiple indices group several related variables.

Each variable has a unique, positive integer called the uniqid. This integer may be used to identify a variable that is represented by more than one data structure. For example, bddvar('a', 0) and exprvar('a', 0) will refer to two different Variable instances, but both will share the same uniqid.

All variables are implicitly ordered. If two variable names are identical, compare their indices. Otherwise, do a string comparison of their names. This is only useful where variable order matters, and is not meaningful in any algebraic sense.

For example, the following statements are true:

• a == a
• a < b
• a[0] < a[1]
• a[0][1] < a[0][2]

name

Return the innermost variable name.

qualname

Return the fully qualified name.

Boolean Functions¶

This is the abstract base class for Boolean function representations.

In addition to the methods and properties listed below, classes inheriting from Function should also overload the __invert__, __or__, __and__, and __xor__ magic methods. This makes it possible to perform symbolic, algebraic manipulations using a Python interpreter.

class pyeda.boolalg.boolfunc.Function[source]

Abstract base class that defines an interface for a symbolic Boolean function of \(N\) variables.

support

Return the support set of a function.

Let \(f(x_1, x_2, \dots, x_n)\) be a Boolean function of \(N\) variables.

The unordered set \(\{x_1, x_2, \dots, x_n\}\) is called the support of the function.

usupport

Return the untyped support set of a function.

inputs

Return the support set in name/index order.

top

Return the first variable in the ordered support set.

degree

Return the degree of a function.

A function from \(B^{N} \Rightarrow B\) is called a Boolean function of degree \(N\).

cardinality

Return the cardinality of the relation \(B^{N} \Rightarrow B\).

Always equal to \(2^{N}\).

iter_domain()[source]

Iterate through all points in the domain.

iter_image()[source]

Iterate through all elements in the image.

iter_relation()[source]

Iterate through all (point, element) pairs in the relation.

restrict(point)[source]

Restrict a subset of support variables to \(\{0, 1\}\).

Returns a new function: \(f(x_i, \ldots)\)

\(f \: | \: x_i = b\)

vrestrict(vpoint)[source]

Expand all vectors in vpoint before applying restrict.

compose(mapping)[source]

Substitute a subset of support variables with other Boolean functions.

Returns a new function: \(f(g_i, \ldots)\)

\(f_1 \: | \: x_i = f_2\)

satisfy_one()[source]

If this function is satisfiable, return a satisfying input point. A tautology may return a zero-dimensional point; a contradiction must return None.

satisfy_all()[source]

Iterate through all satisfying input points.

satisfy_count()[source]

Return the cardinality of the set of all satisfying input points.

iter_cofactors(vs=None)[source]

Iterate through the cofactors of a function over N variables.

The vs argument is a sequence of \(N\) Boolean variables.

The cofactor of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(f_{x_i} = f(x_1, x_2, \dots, 1, \dots, x_n)\)

The cofactor of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i'\) is: \(f_{x_i'} = f(x_1, x_2, \dots, 0, \dots, x_n)\)

cofactors(vs=None)[source]

Return a tuple of the cofactors of a function over N variables.

The vs argument is a sequence of \(N\) Boolean variables.

The cofactor of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(f_{x_i} = f(x_1, x_2, \dots, 1, \dots, x_n)\)

The cofactor of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i'\) is: \(f_{x_i'} = f(x_1, x_2, \dots, 0, \dots, x_n)\)

smoothing(vs=None)[source]

Return the smoothing of a function over a sequence of N variables.

The vs argument is a sequence of \(N\) Boolean variables.

The smoothing of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(S_{x_i}(f) = f_{x_i} + f_{x_i'}\)

This is the same as the existential quantification operator: \(\exists \{x_1, x_2, \dots\} \: f\)

consensus(vs=None)[source]

Return the consensus of a function over a sequence of N variables.

The vs argument is a sequence of \(N\) Boolean variables.

The consensus of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(C_{x_i}(f) = f_{x_i} \cdot f_{x_i'}\)

This is the same as the universal quantification operator: \(\forall \{x_1, x_2, \dots\} \: f\)

derivative(vs=None)[source]

Return the derivative of a function over a sequence of N variables.

The vs argument is a sequence of \(N\) Boolean variables.

The derivative of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(\frac{\partial}{\partial x_i} f = f_{x_i} \oplus f_{x_i'}\)

This is also known as the Boolean difference.

is_zero()[source]

Return whether this function is zero.

Note

This method will only look for a particular “zero form”, and will NOT do a full search for a contradiction.

is_one()[source]

Return whether this function is one.

Note

This method will only look for a particular “one form”, and will NOT do a full search for a tautology.

static box(obj)[source]

Convert primitive types to a Function.

unbox()[source]

Return integer 0 or 1 if possible, otherwise return the Function.

Convert an Expression¶

Since the Boolean expression is PyEDA’s central data type, you can use the expr2bdd function to convert arbitrary expressions to BDDs:

>>> f = expr("a & b | a & c | b & c")
>>> f
Or(And(a, b), And(a, c), And(b, c))
>>> f = expr2bdd(f)
>>> f
<pyeda.boolalg.bdd.BinaryDecisionDiagram at 0x7f556874ed68>

As you can see, the BDD does not have such a useful string representation. More on this subject later.

Using Operators¶

Just like expressions, BDDs have their own Variable implementation. You can use the bddvar function to construct them:

>>> a, b, c = map(bddvar, 'abc')
>>> type(a)
pyeda.boolalg.bdd.BDDVariable
>>> isinstance(a, BinaryDecisionDiagram)
True

Creating indexed variables with namespaces always works just like expressions:

>>> a0 = bddvar('a', 0)
>>> a0
a[0]
>>> b_a_0_1 = bddvar(('a', 'b'), (0, 1))
b.a[0,1]

Also, the bddvars function can be used to create multi-dimensional arrays of indexed variables:

>>> X = bddvars('x', 4, 4)
>>> X
farray([[x[0,0], x[0,1], x[0,2], x[0,3]],
        [x[1,0], x[1,1], x[1,2], x[1,3]],
        [x[2,0], x[2,1], x[2,2], x[2,3]],
        [x[3,0], x[3,1], x[3,2], x[3,3]]])

From variables, you can use Python’s ~|&^ operators to construct arbitrarily large BDDs.

Here is the simple majority function again:

>>> f = a & b | a & c | b & c
>>> f
<pyeda.boolalg.bdd.BinaryDecisionDiagram at 0x7f556874ed68>

This time, we can see the benefit of having variables available:

>>> f.restrict({a: 0})
<pyeda.boolalg.bdd.BinaryDecisionDiagram at 0x7f556874eb38>
>>> f.restrict({a: 1, b: 0})
c
>>> f.restrict({a: 1, b: 1})
1

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]

Complements¶

A complement is defined as the inverse of a variable. That is:

One way to create a complement from a pre-existing 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

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 N-ary (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]

>>> 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'))

>>> s = Xor('a', 'b', 'ci')
>>> co = Or(And('a', 'b'), And('a', 'ci'), And('b', 'ci'))

>>> s = Xor('a', 'b', 'ci')
>>> co = Majority('a', 'b', 'ci')

>>> 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))

>>> 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):

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)

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 sub-expressions 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))

Assumptions¶

A common pattern in SAT-solving 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 command-line 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 well-known DIMACS CNF format. See http://www.satcompetition.org/ for details on expected inputs and outputs. The function is a one-hot 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

Constructor¶

First, create a few expression variables:

>>> a, b, c, d = map(exprvar, 'abcd')

To store these variables in an array, invoke the farray constructor on a sequence:

>>> vs = farray([a, b, c, d])
>>> vs
farray([a, b, c, d])
>>> vs[2]
c

Now let’s store some arbitrary functions into an array. Create six expressions using the secondary operators:

>>> f0 = Nor(a, b, c)
>>> f1 = Nand(a, b, c)
>>> f2 = Xor(a, b, c)
>>> f3 = Xnor(a, b, c)
>>> f4 = Equal(a, b, c)
>>> f5 = Unequal(a, b, c)

To neatly store these six functions in an farray, invoke the constructor like we did before:

>>> F = farray([f0, f1, f2, f3, f4, f5])
>>> F
farray([Nor(a, b, c), Nand(a, b, c), Xor(a, b, c), Xnor(a, b, c), Equal(a, b, c), Unequal(a, b, c)])

This is sufficient for 1-D arrays, but the farray constructor can create mult-dimensional arrays as well. You can apply shape to the input array by either using a nested sequence, or manually using the shape parameter.

To create a 2x3 array using a nested sequence:

>>> F = farray([[f0, f2, f4], [f1, f3, f5]])
>>> F
farray([[Nor(a, b, c), Xor(a, b, c), Equal(a, b, c)],
        [Nand(a, b, c), Xnor(a, b, c), Unequal(a, b, c)]])
>>> F.shape
((0, 2), (0, 3))
>>> F.size
6
>>> F[0,1]
Xor(a, b, c)

Similarly for a 3x2 array:

>>> F = farray([[f0, f1], [f2, f3], [f4, f5]])
>>> F
farray([[Nor(a, b, c), Nand(a, b, c)],
        [Xor(a, b, c), Xnor(a, b, c)],
        [Equal(a, b, c), Unequal(a, b, c)]])
>>> F.shape
((0, 3), (0, 2))
>>> F.size
6
>>> F[0,1]
Nand(a, b, c)

Use the shape parameter to manually impose a shape. It takes a tuple of dimension specs, which are (start, stop) tuples.

>>> F = farray([f0, f1, f2, f3, f4, f5], shape=((0, 2), (0, 3)))
>>> F
farray([[Nor(a, b, c), Xor(a, b, c), Equal(a, b, c)],
        [Nand(a, b, c), Xnor(a, b, c), Unequal(a, b, c)]])

Internally, function arrays are stored in a flat list. You can retrieve the items by using the flat iterator:

>>> list(F.flat)
[Nor(a, b, c),
 Nand(a, b, c),
 Xor(a, b, c),
 Xnor(a, b, c),
 Equal(a, b, c),
 Unequal(a, b, c)]

Use the reshape method to return a new farray with the same contents and size, but with different dimensions:

>>> F.reshape(3, 2)
farray([[Nor(a, b, c), Nand(a, b, c)],
        [Xor(a, b, c), Xnor(a, b, c)],
        [Equal(a, b, c), Unequal(a, b, c)]])

>>> empty = farray([], ftype=Expression)
>>> empty
farray([])
>>> empty.shape
((0, 0),)
>>> empty.size
0

>>> F = farray([f0, f1, f2, f3, f4, f5], shape=((7, 9), (13, 16)))
>>> F
farray([[Nor(a, b, c), Xor(a, b, c), Equal(a, b, c)],
        [Nand(a, b, c), Xnor(a, b, c), Unequal(a, b, c)]])

>>> F.size
6

>>> F.shape
((7, 9), (13, 16))
>>> F[7,14]
Nand(a, b, c)

Factory Functions¶

For convenience, PyEDA provides factory functions for producing arrays with arbitrary shape initialized to all zeros, all ones, or all variables with incremental indices.

The functions for creating arrays of zeros are:

• pyeda.boolalg.bfarray.bddzeros()
• pyeda.boolalg.bfarray.exprzeros()
• pyeda.boolalg.bfarray.ttzeros()

For example, to create a 4x4 farray of expression zeros:

>>> zeros = exprzeros(4, 4)
>>> zeros
farray([[0, 0, 0, 0],
        [0, 0, 0, 0],
        [0, 0, 0, 0],
        [0, 0, 0, 0]])

The variadic dims input is a sequence of dimension specs. A dimension spec is a two-tuple: (start index, stop index). If a dimension is given as a single int, it will be converted to (0, stop).

For example:

>>> zeros = bddzeros((1, 3), (2, 4), 2)
>>> zeros
farray([[[0, 0],
         [0, 0]],

        [[0, 0],
         [0, 0]]])

Similarly for creating arrays of ones:

• pyeda.boolalg.bfarray.bddones()
• pyeda.boolalg.bfarray.exprones()
• pyeda.boolalg.bfarray.ttones()

The functions for creating arrays of variables are:

• pyeda.boolalg.bfarray.bddvars()
• pyeda.boolalg.bfarray.exprvars()
• pyeda.boolalg.bfarray.ttvars()

These functions behave similarly to the zeros/ones functions, but take a name argument as well.

For example, to create a 4x4 farray of expression variables:

>>> A = exprvars('a', 4, 4)
>>> A
farray([[a[0,0], a[0,1], a[0,2], a[0,3]],
        [a[1,0], a[1,1], a[1,2], a[1,3]],
        [a[2,0], a[2,1], a[2,2], a[2,3]],
        [a[3,0], a[3,1], a[3,2], a[3,3]]])

The name argument accepts a tuple of names, just like the exprvar function, and the variadic dims input also supports irregular shapes:

>>> A = exprvars(('a', 'b', 'c'), (1, 3), (2, 4), 2)
>>> A
farray([[[c.b.a[1,2,0], c.b.a[1,2,1]],
         [c.b.a[1,3,0], c.b.a[1,3,1]]],

        [[c.b.a[2,2,0], c.b.a[2,2,1]],
         [c.b.a[2,3,0], c.b.a[2,3,1]]]])

Integer Conversion¶

The previous section discussed ways to initialize arrays to all zeros or ones. It is also possible to create one-dimensional arrays that represent integers using either the unsigned or twos-complement notations.

The following functions convert an unsigned integer to a 1-D farray:

• pyeda.boolalg.bfarray.uint2bdds()
• pyeda.boolalg.bfarray.uint2exprs()
• pyeda.boolalg.bfarray.uint2tts()

The following functions convert a signed integer to a 1-D farray:

• pyeda.boolalg.bfarray.int2bdds()
• pyeda.boolalg.bfarray.int2exprs()
• pyeda.boolalg.bfarray.int2tts()

The signature for these functions are all identical. The num argument is the int to convert, and the length parameter is optional. Unsigned conversion will always zero-extend to the provided length, and signed conversion will always sign-extend.

Here are a few examples of converting integers to expressions:

>>> uint2exprs(42, 8)
farray([0, 1, 0, 1, 0, 1, 0, 0])
>>> int2exprs(42, 8)
farray([0, 1, 0, 1, 0, 1, 0, 0])
# A nifty one-liner to verify the previous conversions
>>> bin(42)[2:].zfill(8)[::-1]
'01010100'
>>> int2exprs(-42, 8)
farray([0, 1, 1, 0, 1, 0, 1, 1])

Function arrays also have to_uint and to_int methods to perform the reverse computation. They do not, however, have any property to indicate whether the array represents signed data. So always know what the encoding is ahead of time. For example:

>>> int2exprs(-42, 8).to_int()
-42
>>> int2exprs(-42, 8).to_uint()
214

Integral Indices¶

Function arrays support a slice syntax that mostly follows the numpy ndarray data type. The primary difference is that farray supports nonzero start indices.

To demonstrate the various capabilities, let’s create some arrays. For simplicity, we will only use zero indexing.

>>> A = exprvars('a', 4)
>>> B = exprvars('b', 4, 4, 4)

Using a single integer index will collapse an array dimension. For 1-D arrays, this means returning an item.

>>> A[2]
a[2]
>>> B[2]
farray([[b[2,0,0], b[2,0,1], b[2,0,2], b[2,0,3]],
        [b[2,1,0], b[2,1,1], b[2,1,2], b[2,1,3]],
        [b[2,2,0], b[2,2,1], b[2,2,2], b[2,2,3]],
        [b[2,3,0], b[2,3,1], b[2,3,2], b[2,3,3]]])
>>> B[2].shape
((0, 4), (0, 4))

The colon : slice syntax shrinks a dimension:

>>> A[:]
farray([a[0], a[1], a[2], a[3]])
>>> A[1:]
farray([a[1], a[2], a[3]])
>>> A[:3]
farray([a[0], a[1], a[2]])
>>> B[1:3]
farray([[[b[1,0,0], b[1,0,1], b[1,0,2], b[1,0,3]],
         [b[1,1,0], b[1,1,1], b[1,1,2], b[1,1,3]],
         [b[1,2,0], b[1,2,1], b[1,2,2], b[1,2,3]],
         [b[1,3,0], b[1,3,1], b[1,3,2], b[1,3,3]]],

        [[b[2,0,0], b[2,0,1], b[2,0,2], b[2,0,3]],
         [b[2,1,0], b[2,1,1], b[2,1,2], b[2,1,3]],
         [b[2,2,0], b[2,2,1], b[2,2,2], b[2,2,3]],
         [b[2,3,0], b[2,3,1], b[2,3,2], b[2,3,3]]]])

For N-dimensional arrays, the slice accepts up to N indices separated by a comma. Unspecified slices at the end will default to :.

>>> B[1,2,3]
b[1,2,3]
>>> B[:,2,3]
farray([b[0,2,3], b[1,2,3], b[2,2,3], b[3,2,3]])
>>> B[1,:,3]
farray([b[1,0,3], b[1,1,3], b[1,2,3], b[1,3,3]])
>>> B[1,2,:]
farray([b[1,2,0], b[1,2,1], b[1,2,2], b[1,2,3]])
>>> B[1,2]
farray([b[1,2,0], b[1,2,1], b[1,2,2], b[1,2,3]])

The ... syntax will fill available indices left to right with :. Only one ellipsis will be recognized per slice.

>>> B[...,1]
farray([[b[0,0,1], b[0,1,1], b[0,2,1], b[0,3,1]],
        [b[1,0,1], b[1,1,1], b[1,2,1], b[1,3,1]],
        [b[2,0,1], b[2,1,1], b[2,2,1], b[2,3,1]],
        [b[3,0,1], b[3,1,1], b[3,2,1], b[3,3,1]]])
>>> B[1,...]
farray([[b[1,0,0], b[1,0,1], b[1,0,2], b[1,0,3]],
        [b[1,1,0], b[1,1,1], b[1,1,2], b[1,1,3]],
        [b[1,2,0], b[1,2,1], b[1,2,2], b[1,2,3]],
        [b[1,3,0], b[1,3,1], b[1,3,2], b[1,3,3]]])

Function arrays support negative indices. Arrays with a zero start index follow Python’s usual conventions.

For example, here is the index guide for A[0:4]:

 +------+------+------+------+
 | a[0] | a[1] | a[2] | a[3] |
 +------+------+------+------+
 0      1      2      3      4
-4     -3     -2     -1

And example usage:

>>> A[-1]
a[3]
>>> A[-3:-1]
farray([a[1], a[2]])

Arrays with non-zero start indices also support negative indices. For example, here is the index guide for A[3:7]:

 +------+------+------+------+
 | a[3] | a[4] | a[5] | a[6] |
 +------+------+------+------+
 3      4      5      6      7
-4     -3     -2     -1

Multiplexor Selects¶

A special feature of array slicing is the ability to multiplex array items over a select input. For a 2:1 mux, the select may be a single function. Otherwise, it must be an farray with enough bits.

For example, to create a simple 8:1 mux:

>>> X = exprvars('x', 8)
>>> sel = exprvars('s', 3)
>>> X[sel]
Or(And(~s[0], ~s[1], ~s[2], x[0]),
   And( s[0], ~s[1], ~s[2], x[1]),
   And(~s[0],  s[1], ~s[2], x[2]),
   And( s[0],  s[1], ~s[2], x[3]),
   And(~s[0], ~s[1],  s[2], x[4]),
   And( s[0], ~s[1],  s[2], x[5]),
   And(~s[0],  s[1],  s[2], x[6]),
   And( s[0],  s[1],  s[2], x[7]))

This works for multi-dimensional arrays as well:

>>> s = exprvar('s')
>>> Y = exprvars('y', 2, 2, 2)
>>> Y[:,s,:]
farray([[Or(And(~s, y[0,0,0]),
            And( s, y[0,1,0])),
         Or(And(~s, y[0,0,1]),
            And( s, y[0,1,1]))],

        [Or(And(~s, y[1,0,0]),
            And( s, y[1,1,0])),
         Or(And(~s, y[1,0,1]),
            And( s, y[1,1,1]))]])

Unary Reduction¶

A common operation is to reduce the entire contents of an array to a single function. This is supported by the OR, AND, and XOR operators because they are 1) variadic, and 2) associative.

Unfortunately, Python has no appropriate symbols available, so unary operators are supported by the following farray methods:

• pyeda.boolalg.bfarray.farray.uor()
• pyeda.boolalg.bfarray.farray.unor()
• pyeda.boolalg.bfarray.farray.uand()
• pyeda.boolalg.bfarray.farray.unand()
• pyeda.boolalg.bfarray.farray.uxor()
• pyeda.boolalg.bfarray.farray.uxnor()

For example, to OR the contents of an eight-bit array:

>>> X = exprvars('x', 8)
>>> X.uor()
Or(x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7])

One well-known usage of unary reduction is conversion from a binary-reflected gray code (BRGC) back to binary. In the following example, B is a 3-bit array that contains logic to convert the contents of G from gray code to binary. See the Wikipedia Gray Code article for background.

>>> G = exprvars('g', 3)
>>> B = farray([G[i:].uxor() for i, _ in enumerate(G)])
>>> graycode = ['000', '100', '110', '010', '011', '111', '101', '001']
>>> for gs in graycode:
...     print(B.vrestrict({X: gs}).to_uint())
0
1
2
3
4
5
6
7

Bit-wise Logic¶

Arrays are an algebraic data type. They overload several of Python’s operators to perform bit-wise logic.

First, let’s create a few arrays:

>>> A = exprvars('a', 4)
>>> B = exprvars('b', 4)
>>> C = exprvars('c', 2, 2)
>>> D = exprvars('d', 2, 2)

To invert the contents of A:

>>> ~A
farray([~a[0], ~a[1], ~a[2], ~a[3]])

Inverting a multi-dimensional array will retain its shape:

>>> ~C
farray([[~c[0,0], ~c[0,1]],
        [~c[1,0], ~c[1,1]]])

The binary OR, AND, and XOR operators work for arrays with equal size:

>>> A | B
farray([Or(a[0], b[0]), Or(a[1], b[1]), Or(a[2], b[2]), Or(a[3], b[3])])
>>> A & B
farray([And(a[0], b[0]), And(a[1], b[1]), And(a[2], b[2]), And(a[3], b[3])])
>>> C ^ D
farray([[Xor(c[0,0], d[0,0]), Xor(c[0,1], d[0,1])],
        [Xor(c[1,0], d[1,0]), Xor(c[1,1], d[1,1])]])

Mismatched sizes will raise an exception:

>>> A & B[2:]
Traceback (most recent call last):
    ...
ValueError: expected operand sizes to match

For arrays of the same size but different shape, the resulting shape is ambiguous so by default the result is flattened:

>>> Y = ~A | C
>>> Y
farray([Or(~a[0], c[0,0]), Or(~a[1], c[0,1]), Or(~a[2], c[1,0]), Or(~a[3], c[1,1])])
>>> Y.size
4
>>> Y.shape
((0, 4),)

Shifts¶

Function array have three shift methods:

• pyeda.boolalg.bfarray.farray.lsh(): logical left shift
• pyeda.boolalg.bfarray.farray.rsh(): logical right shift
• pyeda.boolalg.bfarray.farray.arsh(): arithmetic right shift

The logical left/right shift operators shift out num items from the array, and optionally shift in values from a cin (carry-in) parameter. The output is a two-tuple of the shifted array, and the “carry-out”.

The “left” direction in lsh shifts towards the most significant bit. For example:

>>> X = exprvars('x', 8)
>>> X.lsh(4)
(farray([0, 0, 0, 0, x[0], x[1], x[2], x[3]]),
 farray([x[4], x[5], x[6], x[7]]))
>>> X.lsh(4, exprvars('y', 4))
(farray([y[0], y[1], y[2], y[3], x[0], x[1], x[2], x[3]]),
 farray([x[4], x[5], x[6], x[7]]))

Similarly, the “right” direction in rsh shifts towards the least significant bit. For example:

>>> X.rsh(4)
(farray([x[4], x[5], x[6], x[7], 0, 0, 0, 0]),
 farray([x[0], x[1], x[2], x[3]]))
>>> X.rsh(4, exprvars('y', 4))
(farray([x[4], x[5], x[6], x[7], y[0], y[1], y[2], y[3]]),
 farray([x[0], x[1], x[2], x[3]]))

You can use the Python overloaded << and >> operators for lsh, and rsh, respectively. The only difference is that they do not produce a carry-out. For example:

>>> X << 4
farray([0, 0, 0, 0, x[0], x[1], x[2], x[3]])
>>> X >> 4
farray([x[4], x[5], x[6], x[7], 0, 0, 0, 0])

Using a somewhat awkward (num, farray) syntax, you can use these operators with a carry-in. For example:

>>> X << (4, exprvars('y', 4))
farray([y[0], y[1], y[2], y[3], x[0], x[1], x[2], x[3]])
>>> X >> (4, exprvars('y', 4))
farray([x[4], x[5], x[6], x[7], y[0], y[1], y[2], y[3]])

An arithmetic right shift automatically sign-extends the array. Therefore, it does not take a carry-in. For example:

>>> X.arsh(4)
(farray([x[4], x[5], x[6], x[7], x[7], x[7], x[7], x[7]]),
 farray([x[0], x[1], x[2], x[3]]))

Due to its importance in digital design, Verilog has a special >>> operator for an arithmetic right shift. Sadly, Python has no such indulgence. If you really want to use a symbol, you can use the cin parameter to achieve the same effect with >>:

>>> num = 4
>>> X >> (num, num * X[-1])
farray([x[4], x[5], x[6], x[7], x[7], x[7], x[7], x[7]])

Concatenation and Repetition¶

Two very important operators in hardware description languages are concatenation and repetition of logic vectors. For example, in this implementation of the xtime function from the AES standard, xtime[6:0] is concatenated with 1'b0, and xtime[7] is repeated eight times before being AND’ed with 8'h1b.

function automatic logic [7:0]
xtime(logic [7:0] b, int n);
    xtime = b;
    for (int i = 0; i < n; i++)
        xtime = {xtime[6:0], 1'b0}       // concatenation
              ^ (8'h1b & {8{xtime[7]}}); // repetition
endfunction

The farray data type resembles the Python tuple for these operations.

To concatenate two arrays, use the + operator:

>>> X = exprvars('x', 4)
>>> Y = exprvars('y', 4)
>>> X + Y
farray([x[0], x[1], x[2], x[3], y[0], y[1], y[2], y[3]])

It is also possible to prepend or append single functions:

>>> a, b = map(exprvar, 'ab')
>>> a + X
farray([a, x[0], x[1], x[2], x[3]])
>>> X + b
farray([x[0], x[1], x[2], x[3], b])
>>> a + X + b
farray([a, x[0], x[1], x[2], x[3], b])
>>> a + b
farray([a, b])

Even 0 (or False) and 1 (or True) work:

>>> 0 + X
farray([0, x[0], x[1], x[2], x[3]])
>>> X + True
farray([x[0], x[1], x[2], x[3], 1])

To repeat arrays, use the * operator:

>>> X * 2
farray([x[0], x[1], x[2], x[3], x[0], x[1], x[2], x[3]])
>>> 0 * X
farray([])

Similarly, this works for single functions as well:

>>> a * 3
farray([a, a, a])
>>> 2 * a + b * 3
farray([a, a, b, b, b])

Multi-dimensional arrays are automatically flattened during either concatenation or repetition:

>>> Z = exprvars('z', 2, 2)
>>> X + Z
farray([x[0], x[1], x[2], x[3], z[0,0], z[0,1], z[1,0], z[1,1]])
>>> Z * 2
farray([z[0,0], z[0,1], z[1,0], z[1,1], z[0,0], z[0,1], z[1,0], z[1,1]])

If you require a more subtle treatment of the shapes, use the reshape method to unflatten things:

>>> (Z*2).reshape(2, 4)
farray([[z[0,0], z[0,1], z[1,0], z[1,1]],
        [z[0,0], z[0,1], z[1,0], z[1,1]]])

Function arrays also support the “in-place” += and *= operators. The farray behaves like an immutable object. That is, it behaves more like the Python tuple than a list.

For example, when you concatenate/repeat an farray, it returns a new farray:

>>> A = exprvars('a', 4)
>>> B = exprvars('b', 4)
>>> id(A)
3050928972
>>> id(B)
3050939660
>>> A += B
>>> id(A)
3050939948
>>> B *= 2
>>> id(B)
3050940716

The A += B implementation is just syntactic sugar for:

>>> A = A + B

And the A *= 2 implementation is just syntactic sugar for:

>>> A = A * 2

To wrap up, let’s re-write the xtime function using PyEDA function arrays.

def xtime(b, n):
    """Return b^n using polynomial multiplication in GF(2^8)."""
    for _ in range(n):
        b = exprzeros(1) + b[:7] ^ uint2exprs(0x1b, 8) & b[7]*8
    return b

One Hot Function¶

Let’s say I have three variables, a, b, and c.

>>> a, b, c = map(exprvar, 'abc')

I want to write a Boolean formula that guarantees that only one of them is true at any given moment.

>>> f = OneHot(a, b, c)

You can use PyEDA to automatically produce the truth table.

>>> expr2truthtable(f)
c 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 : 0

By default, the OneHot function returns a formula in conjunctive normal (product-of-sums) form. Roughly translated, this formula says that “no two variables can both be true, and at least one must be true”.

>>> f
And(Or(~a, ~b), Or(~a, ~c), Or(~b, ~c), Or(a, b, c))

In disjunctive normal (sum-of-products) form, the function looks like this:

>>> f.to_dnf()
Or(And(~a, ~b, c), And(~a, b, ~c), And(a, ~b, ~c))

Value Constraints¶

You probably already noticed that if the square at (5, 3) has value ‘8’, it is not allowed to have any other value. That is, if X[5,3,8] = 1, then X[5,3,1:10] == [0, 0, 0, 0, 0, 0, 0, 1, 0].

We need to write a constraint formula that says “every square on the board can assume only one value.” With PyEDA, you can write this formula as follows:

>>> V = And(*[
...         And(*[
...             OneHot(*[ X[r, c, v]
...                 for v in range(1, 10) ])
...             for c in range(1, 10) ])
...         for r in range(1, 10) ])

Row and Column Constraints¶

Next, we need to write formulas that say “every square in each row is unique”, and “every square in each column is unique”, respectively.

>>> R = And(*[
...         And(*[
...             OneHot(*[ X[r, c, v]
...                 for c in range(1, 10) ])
...             for v in range(1, 10) ])
...         for r in range(1, 10) ])

>>> C = And(*[
...         And(*[
...             OneHot(*[ X[r, c, v]
...                 for r in range(1, 10) ])
...             for v in range(1, 10) ])
...         for c in range(1, 10) ])

Box Constraints¶

The box constraints are a little tricker. We need a formula that says “every square in a box is unique”. The key to understanding how to write this formula is to think of the grid as consisting of 3x3 boxes. Now instead of iterating over the nine squares in a row or column, we will iterate over the 3 rows and 3 columns of the 3x3 boxes.

>>> B = And(*[
...         And(*[
...             OneHot(*[ X[3*br+r, 3*bc+c, v]
...                 for r in range(1, 4) for c in range(1, 4) ])
...             for v in range(1, 10) ])
...         for br in range(3) for bc in range(3) ])

Putting It All Together¶

Now that we have the value, row, column, and box constraints, we need to combine them all into a single formula. We will use the And function to join the constraints, because all constraints must be true for the puzzle to be solved.

>>> S = And(V, R, C, B)
>>> len(S.xs)
10530

As you can see, the constraints formula is quite large.

Row and Column Constraints¶

Rather than start with the constraint that \(\sum X_{i,j} = 8\), we will instead start with a simplifying observation. In order to place eight queens on the board, since there are exactly eight rows and eight columns on the board itself, it is obvious that exactly one queen must be placed on each row, and each column.

First, we write a constraint that says “exactly one queen must be placed on each row”.

>>> R = And(*[OneHot(*[X[r,c] for c in range(8)]) for r in range(8)])

Next, we write a constraint that says “exactly one queen must be placed on each column”.

>>> C = And(*[OneHot(*[X[r,c] for r in range(8)]) for c in range(8)])

Diagonal Constraints¶

Diagonal constraints are easy to visualize, but slightly trickier to specify mathematically. We will break down the diagonal constraints into two separate sets:

• left-to-right
• right-to-left

In both cases, the diagonal is always oriented “bottom-to-top”.

In both cases, we need to write a constraint that says “at most one queen can be located on each diagonal”.

>>> starts = [(i, 0) for i in range(8-2, 0, -1)] + [(0, i) for i in range(8-1)]
>>> lrdiags = []
>>> for r, c in starts:
...     lrdiags.append([])
...     ri, ci = r, c
...     while ri < 8 and ci < 8:
...         lrdiags[-1].append((ri, ci))
...         ri += 1
...         ci += 1
...
>>> DLR = And(*[OneHot0(*[X[r,c] for r, c in diag]) for diag in lrdiags])

>>> starts = [(i, 8-1) for i in range(8-2, -1, -1)] + [(0, i) for i in range(8-2, 0, -1)]
>>> rldiags = []
>>> for r, c in starts:
...     rldiags.append([])
...     ri, ci = r, c
...     while ri < 8 and ci >= 0:
...         rldiags[-1].append((ri, ci))
...         ri += 1
...         ci -= 1
...
>>> DRL = And(*[OneHot0(*[X[r,c] for r, c in diag]) for diag in rldiags])