search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

Z3-opt for Integer #391

Closed gingeredder closed 8 years ago

gingeredder commented 8 years ago

As far as I was concerned, the Z3-opt is for the LRA theory. Obviously, it could be used to solve the Integer Linear Programming. But the performance based on rational number may be no better than based on pure integer? Does the Z3-opt have the branch for pure integer without rational number?(namely, specific for Integer Linear Programming)

cheshire commented 8 years ago

I am not a Z3 developer, but Z3 supports integer programming very well, I mostly use it myself for optimizations modulo LIA. There is no specific branch for integers.

NikolajBjorner commented 8 years ago

LIA support is included, performance depends on efficiency of underlying solver. For integer difference logic (IDL) one can try also underlying solvers for this fragment though mostly the default configuration seems better. Pseudo booleans are also handled, eg if you use integers bound between 0 and 1.