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)