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.