z3 SMT Sat Solver Interface

The z3 Satisfiability Solver interface can convert pyomo variables and expressions for use with the z3 Satisfiability Solver

Installation

z3 is required for use of the Sat Solver can be installed via the command

pip install z3-solver

Using z3 Sat Solver

To use the sat solver define your pyomo model as usual:

Required import
>>> import pyomo.environ as pyo
>>> from pyomo.contrib.satsolver.satsolver import SMTSatSolver

Create a simple model
>>> m = pyo.ConcreteModel()
>>> m.x = pyo.Var()
>>> m.y = pyo.Var()
>>> m.obj = pyo.Objective(expr=m.x**2 + m.y**2)
>>> m.c = pyo.Constraint(expr=m.y >= -2*m.x + 5)

Invoke the sat solver using optional argument model to automatically process
pyomo model
>>> is_feasible = SMTSatSolver(model = m).check()