# Z3 timed out? Try Gurobi

I had many SMT formulas that cannot be solved by Z3. They just hanged. But after I reformulate them as 0–1 ILP, Gurobi can efficiently solve them.

SAT problem is a particular case of 0–1 Integer Linear Program (ILP). It can be formulated as a 0-1 ILP feasibility problem, with no optimization objective. The variables in the ILP are boolean, and the constraints are the clauses and their dependencies.

Some standard encodings:

**AND:**y = x₁∧x₂∧…∧xₙ. Constraint: 0 ≤ Σxᵢ - ny ≤ n-1**OR:**y = x₁∨x₂∨…∨xₙ. Constraint: 0 ≤ ny - Σxᵢ ≤ n-1**NOT:**y= ¬ x. Constraint: y = 1 - x

So each atom in the SMT formula can be a boolean variable in ILP. Perhaps the most important thing is to model the dependencies between atoms, sometimes due to the dependencies of the inputs, which varies across different applications.