z3

A Constraint Solver created by Microsoft.

Installation

1. pip install z3 z3-solver

Solver Process

1. Declare variables
2. Create solver object
3. Add constraints to solver
4. Solve the solver

Boilerplate

from z3 import *
 
# Create a solver instance
solver = Solver()
 
# Define the variables
x = Int('x')
y = Int('y')
 
# Add constraints
solver.add(x + y == 10)
solver.add(x > 0)
solver.add(y > 0)
 
# Check if the constraints are satisfiable
if solver.check() == sat:
    # Get the model (solution)
    model = solver.model()
    print(f'Solution: x = {model[x]}, y = {model[y]}')
else:
    print('No solution found')