Modelling Module

OptiLog provides a high level API for modelling non-CNF formulas.

This module provides functionality for:

  • Converting Non-CNF formulas to CNF formulas

  • Representing Formulas with varying levels of parenthesis

  • Encoding non normalized Pseudo Boolean expressions and normalizing them

  • Representing truth tables of multiple problems with common variables

  • Encoding (decoding) to (from) DIMACS

  • Evaluate formulas with a high level interpretation

  • Other features…

Basic Problem Modelling

For simplicity, the modelling module is usually imported with the star operator like to import everything, like so:

>>> from optilog.modelling import *

This allows us to instantiate boolean variables:

>>> a = Bool('a')
>>> b = Bool('b')
>>> c = Bool('c')
>>> z = Bool('z')

And then use these variables to model expressions:

>>> expr1 = ~a & b & c | z
>>> print(expr1) # ~a & b & c | z

We can also combine expressions

>>> e1 = a | b
>>> e2 = c & e1
>>> e2
c & (a | b)

These expressions can also be represented by forcing parenthesis.

>>> print(expr1.represent(parenthesis='force')) # ((~a & b & c) | z)

This functionality is very useful for undergraduate Computer Science courses that introduce propositional logic. By enforcing parentheses representation, teachers and students can check the correct operator precedence of the formulas.

The next possible step is to model Problems. Problems are a collection of expressions as constraints. In this example we will add the previously created expression and a new one:

>>> p = Problem()
>>> p.add_constr(expr1)
~a & b & c | z
>>> p.add_constr(a | b)
a | b

Once the problem has been instantiated, we can visualize its TruthTable:

>>> t = TruthTable(p)
>>> t.print()
| z | b | c | a | (~a & b & c | z) & (a | b) |
+---+---+---+---+----------------------------+
| 0 | 0 | 0 | 0 |             0              |
| 0 | 0 | 0 | 1 |             0              |
| 0 | 0 | 1 | 0 |             0              |
| 0 | 0 | 1 | 1 |             0              |
| 0 | 1 | 0 | 0 |             0              |
| 0 | 1 | 0 | 1 |             0              |
| 0 | 1 | 1 | 0 |             1              |
| 0 | 1 | 1 | 1 |             0              |
| 1 | 0 | 0 | 0 |             0              |
| 1 | 0 | 0 | 1 |             1              |
| 1 | 0 | 1 | 0 |             0              |
| 1 | 0 | 1 | 1 |             1              |
| 1 | 1 | 0 | 0 |             1              |
| 1 | 1 | 0 | 1 |             1              |
| 1 | 1 | 1 | 0 |             1              |
| 1 | 1 | 1 | 1 |             1              |

The order of the variables of the TruthTable can also be configured:

>>> t.print(variable_order=[a,b,c,z])

We also could have evaluated the problem manually:

>>> res = p.evaluate({
>>>     'a': True,
>>>     'b': False,
>>>     'c': False,
>>>     'z': False
>>> })
>>> print(res) # False

Operators and parsing options

The following operators (and symbols) are provided:

  • Logic And (&)

  • Logic Or (|)

  • Logic Xor (^)

  • Logic Not (~)

  • Logic If

  • Logic Iff

  • Comparison Constraints such as Equality, LessThan, GreaterThan, LessOrEqual, GreaterOrEqual

  • Other Integer operators like Add, Substract, Multiply, Power and Minus

Expressions can be crafted with the symbols or with the underlying classes. In the following example all of the expressions are equivalent:

>>> expr = ~a & b & c | z
>>> expr = And(~a,b,c) | z
>>> expr = Or(And(~a,b,c),z)
>>> expr = Or(And(Not(a),b,c),z)

OptiLog also supports If and Iff Operators, without symbol overloading like so:

>>> expr = If(a, b) # a -> b
>>> expr = Iff(a, b) # a <-> b

In order to ease the modelling of complex formulas, a parsing option is available.

>>> expr = Bool.parse('a -> b & c | d')
>>> print(expr) # a -> b & c | d
>>> print(expr.represent(parenthesis='force')) # (a -> ((b & c) | d))

This way of generating expressions preserves parentheses by default. Notice the following code prints a different expression:

>>> expr = Bool.parse('a -> ((b & c) | d)')
>>> print(expr) # a -> ((b & c) | d)

But it is equivalent:

>>> print(expr.represent(parenthesis='simplify')) # a -> b & c | d

Equivalence of Python operators, Expression classes, and textual description

Using the modelling module, you can describe problems in three possible ways: creating Bool variables and applying python operators, using the Expression classes (such as And, If…), or using a textual description of the encoding as a string and calling Bool.parse. The following table shows the equivalence between the three variants:

Equivalence

Operation

Python operator

Expression class

Textual string

Negation of a literal a

~a

Not(a)

“~a”

Conjunction of two literals a, b, c

a & b

And(a, b) 1

“a & b”

Disjunction of two literals a, b

a | b

Or(a, b) 1

“a | b”

a implies b

Not available

If(a, b)

“a -> b”

Double implication between a and b

Not available

Iff(a, b)

“a <-> b”

Xor between a and b

a ^ b

Xor(a, b) 1

“a ^ b”

Addition

a + b

Add(a, b) 1

“a + b”

Minus (unary)

-a

Minus(a)

“-a”

Subtraction

a - b

Substract(a, b)

“a - b”

Multiplication

a * b

Multiply(a, b) 1

“a * b”

Division

Not available

Not available

Not available

Power

a ** b

Power(a, b)

“a ** b”

Equivalence: \(a + b = c\)

(a + b) == c

Equality(a + b, c)

“(a + b) == c”

Less than: \(a + b < c\)

(a + b) < c

LessThan(a + b, c)

“(a + b) < c”

Greater than: \(a + b > c\)

(a + b) > c

GreaterThan(a + b, c)

“(a + b) > c”

Less or equal than: \(a + b <= c\)

a + b <= c

LessOrEqual(a + b, c)

“(a + b) <= c”

Greater or equal than: \(a + b >= c\)

a + b >= c

GreaterOrEqual(a + b, c)

“(a + b) >= c”

You can nest and combine different operations at once. The priority levels that will be applied are:

  1. Parenthesis

  2. Power

  3. Minus (unary), Negation

  4. Multiplication

  5. Addition and subtraction

  6. Conjunction

  7. Xor

  8. Disjunction

  9. Implication and double implication

Solving a Problem with a SAT solver

We can leverage this modelling module to solve non-CNF formulas with the standard SAT solvers integrated into OptiLog.

The first thing we need to do is define a problem and convert it to DIMACS:

>>> p = Problem()
>>> p.add_constr(~a & b & c | z)
>>> p.add_constr(a | b)
>>> cnf = p.to_cnf_dimacs()

Finally, we can solve this cnf encoded instance with a solver such as Glucose41:

>>> from optilog.solvers.sat import Glucose41
>>> s = Glucose41()
>>> s.add_clauses(cnf.clauses)
>>> s.solve()
>>> interpretation = cnf.decode_dimacs(s.model())
>>> print('Interpretation:', interpretation) # [~z, b, c, ~a]

Notice the call to the method decode_dimacs that translates the DIMACS encoded solution into a higher level interpretation.

The formula is translated by Tseytin transformation

Encoding Pseudo Boolean Expressions

OptiLog has support for encoding non normalized Pseudo Boolean expressions.

The following example encodes a cardinality constraint. The constraint is interpreted as an expression and is then instantiated as a Problem:

>>> a = Bool('a')
>>> b = Bool('b')
>>> c = Bool('c')
>>> p = Problem(a + b + c < 2, name='cardinality')
>>> t = TruthTable(p)
>>> t.print()

Prints:

>>> | a | b | c | cardinality |
>>> +---+---+---+-------------+
>>> | 0 | 0 | 0 |      1      |
>>> | 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      |

More complex Pseudo Boolean expressions are also supported and are automatically normalized. Example:

>>> p = Problem(a + b * 2 + c <= ~b + 3)
>>> t = TruthTable(p)
>>> t.print()

Prints:

>>> | a | c | b | a + b * 2 + c <= ~b + 3 |
>>> +---+---+---+-------------------------+
>>> | 0 | 0 | 0 |            1            |
>>> | 0 | 0 | 1 |            1            |
>>> | 0 | 1 | 0 |            1            |
>>> | 0 | 1 | 1 |            1            |
>>> | 1 | 0 | 0 |            1            |
>>> | 1 | 0 | 1 |            1            |
>>> | 1 | 1 | 0 |            1            |
>>> | 1 | 1 | 1 |            0            |

Footnotes

1(1,2,3,4,5)

This Expression class accepts a variable amount of operands: Class(a, b, c, d…)