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:
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:
Parenthesis
Power
Minus (unary), Negation
Multiplication
Addition and subtraction
Conjunction
Xor
Disjunction
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()
| 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()
| 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 |
PB Normalization is also supported when translating to CNF:
>>> from optilog.modelling import *
>>> problem = Problem(a + b * 2 + c <= ~ b + 3)
>>> problem.to_cnf_dimacs()
p cnf 12 25
-3 -4 0
3 4 0
-1 -5 0
1 5 0
-3 -6 0
3 6 0
-2 -7 0
2 7 0
-8 -6 0
8 6 0
-9 -7 -4 0
9 7 0
9 4 0
-10 -7 -5 0
10 7 0
10 5 0
-11 -4 -5 0
11 4 0
11 5 0
12 -8 -9 -10 -11 0
-12 8 0
-12 9 0
-12 10 0
-12 11 0
12 0
PB Normalization does not apply the distributive rule, coefficients must multiply only a single variable.
Footnotes