The z3 Satisfiability Solver interface can convert pyomo variables and expressions for use with the z3 Satisfiability Solver
z3 is required for use of the Sat Solver can be installed via the command
pip install z3-solver
To use the sat solver define your pyomo model as usual:
Required import >>> from pyomo.environ import * >>> from pyomo.contrib.satsolver.satsolver import SMTSatSolver
Create a simple model >>> m = ConcreteModel() >>> m.x = Var() >>> m.y = Var() >>> m.obj = Objective(expr=m.x*2 + m.y2) >>> m.c = Constraint(expr=m.y >= -2m.x + 5)
Invoke the sat solver using optional argument model to automatically process pyomo model >>> is_feasible = SMTSatSolver(model = m).check()# doctest: +SKIP