Boolean Logic with PySMT¶
This tutorial will guide you through the basic features of PySMT!
Basic Solving¶
PySMT is a library that simplifies the use of modern Satisfiability Modulo Theory technology.
In this first demo, we will introduce basic solving, that is how to create a simple logical formula, with variables, how to check if a model for such a formula exists and, if it does, how to retrieve a satisfying assignemnt for the variables.
As for any python library, the very first step is to import the functions and classes we need for our application. PySMT is designed to be highly structured and reentrant, but offers a simplified API that serves most of the classical usage of an SMT solver. Such API groups in a single module all the functions to construct formulae, to check the satisfiability and to retrieve Solver instances.
The module to import is pysmt.shortcuts
.
In our example, we need six functions: Symbol
, And
,
Not
, Or
, is_sat
and get_model
.
from pysmt.shortcuts import Symbol, And, Not, Or, is_sat, get_model
The first formula we want to check in this example is the classic unsatisfiable formula: \(a \wedge \neg a\)
For this purpose, we first need to create a new variable \(a\).
PySMT variables are called “symbols” and are created using the
Symbol
shortcut. The function takes in input a variable name and
optionally a type that will be useful when we’ll introduce SMT theories.
By default, the symbols are Booleans, hence the following code creates
and returns the PySMT representation for a variable \(a\).
a = Symbol("a")
At this point, we can create our formula. PySMT offers a number of
functions to construct formulae like conjunction (And
), disjunction
(Or
), negation (Not
) and so on. Each builds a PySMT
representation of a formula given as arguments other formulae. For
example, Not(a)
returns the PySMT representation of \(\neg a\).
We can build the formula \(a \wedge \neg a\) as follows.
phi = And(a, Not(a))
Each formula in PySMT can be easily printed or converted to a
human-readble string. Very large formulae are not printed completely by
default, but the serialize
method allows to get the full
serialization.
print(phi)
string_repr = str(phi)
serialized_strinf = phi.serialize()
(a & (! a))
Given a first order formula, checking its satisfiability means checking if there exists an interpretation for its non-logical symbols that makes the formula true. Our example is actually a propositional formula, and checking satisfiability amounts to check if there is a truth value for the variables appearing in the formula that makes the formula true.
Clearly, our example formula is not satisfiable (it is UNSAT), because assigning \(a = \top\) makes the formula false as assigning \(a = \bot\).
The basic goal of PySMT is to provide you the possibility of quickly and
simply checking satisfiability of formulae. The is_sat
function is
the simpler way of checking the satisfiability of any given formula. It
takes a formula and returns True
if it is satisfiable, otherwise it
returns False
.
check = is_sat(phi)
assert check is False
Now, to show what happens with a satisfiable formula, we create the representation for \((a \wedge \neg a) \vee b\). This formula is clearly satisfiable, because assigning \(b = \top\) is sufficient to make the formula true.
b = Symbol("b")
psi = Or(phi, b)
At this point, we can check that the formula is satisfiable. We could
use again the is_sat
function, but this time we’ll show another
useful shortcut that provides information about the satisfiability, but
also creates and returns a satisfying model for the formula.
This function is called get_model
and given a formula, it returns
None
if the formula is UNSAT, otherwise it returns an object
implementing the Model
interface, that can be queried to retrive a
satisfying assignment. We shall see the Model
interface in detail,
but for now we will use some basic features.
m = get_model(psi)
assert m is not None
Given a model m
, we can retrive the python value for a variable
using the get_py_value
method. The method takes in input any PySMT
formula and constructs a python representation for the value of the term
in the model.
In our example, the variable \(b\) must be set to true to make the
formula true, hence the python value of the variable b
must be
True
.
assert m.get_py_value(b)