.. include:: shared/references.rst

.. _modelling-module:

Modelling Module
==========================

.. py:module:: optilog.modelling

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:
    
.. code:: python
  :number-lines:

  >>> from optilog.modelling import *

This allows us to instantiate boolean variables:

.. code:: python
  :number-lines:

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

And then use these variables to model expressions:

.. code:: python
  :number-lines:

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

We can also combine expressions

.. code:: python
  :number-lines:

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

These expressions can also be represented by forcing parenthesis.

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

We also could have evaluated the problem manually:

.. code:: python
  :number-lines:

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

.. warning::
  Currently XOR is not supported when translating to CNF.
  This limitation will be lifted in the future.

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

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

.. note:
    Notice that the arity of the operands varies per operator.
    * Not has an arity of 1
    * If and Iff have an arity of 2
    * And, Or, Xor are n-ary operators

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

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

But it is equivalent:

.. code:: python
  :number-lines:

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

.. list-table:: Equivalence
    :widths: 25 25 25 25
    :header-rows: 1

    * - 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)` [#multiarg]_
      - `"a & b"`
    * - Disjunction of two literals `a`, `b`
      - `a | b`
      - `Or(a, b)` [#multiarg]_
      - `"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)` [#multiarg]_
      - `"a ^ b"`
    * - Addition
      - `a + b`
      - `Add(a, b)` [#multiarg]_
      - `"a + b"`
    * - Minus (unary)
      - `-a`
      - `Minus(a)`
      - `"-a"`
    * - Subtraction
      - `a - b`
      - `Substract(a, b)`
      - `"a - b"`
    * - Multiplication
      - `a * b`
      - `Multiply(a, b)` [#multiarg]_
      - `"a * b"`
    * - Division
      - *Not available*
      - *Not available*
      - *Not available*
    * - Power
      - `a ** b`
      - `Power(a, b)`
      - `"a ** b"`
    * - Equivalence: :math:`a + b = c`
      - `(a + b) == c`
      - `Equality(a + b, c)`
      - `"(a + b) == c"`
    * - Less than: :math:`a + b < c`
      - `(a + b) < c`
      - `LessThan(a + b, c)`
      - `"(a + b) < c"`
    * - Greater than: :math:`a + b > c`
      - `(a + b) > c`
      - `GreaterThan(a + b, c)`
      - `"(a + b) > c"`
    * - Less or equal than: :math:`a + b <= c`
      - `a + b <= c`
      - `LessOrEqual(a + b, c)`
      - `"(a + b) <= c"`
    * - Greater or equal than: :math:`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:

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

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:

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

.. code:: python
  :number-lines:

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

.. rubric:: Footnotes
.. [#multiarg] This Expression class accepts a variable amount of operands: `Class(a, b, c, d...)`