z3 is super slow on .lp file

[madeken]

I'm not sure if this is a bug per-se, but is it expected that z3 is super slow on a .lp file with a lot of binary variables?

The file: https://gist.github.com/madeken/0196f9b35e96bde22264f12e336b185e

I'm running it with z3 -lp superslow.lp and giving up before it gives a result. Other solvers like scip are providing optimal solutions in under 0.2 seconds.

[NikolajBjorner]

I don't expect it to be fast on such problems. For this particular instance, you use a lot of large coefficients. Their sum exceed 2^32 and in this case z3 switches to a bit-vector encoding instead of using a Pseudo-Boolean solver. The bit-vector encoding is super expensive and not the best way to solve the problem (extending to 64bit instead of 32bit may deal with the toggle issue, but this is the first use case I have seen to take that tangent). The Pseudo-Boolean solver in z3 uses only propagation and lemma learning. It does not use linear relaxations. MIP solvers should at least take advantage of linear relaxations as well for this class of instances. But you are welcome to add an LP component to the PB solver :-).

[madeken]

@NikolajBjorner Thanks for the explanation. Is there any way to compile z3 to work with 64bit instead of 32bit numbers, as my problem space by necessity deals with pretty large numbers (up to 2^51 actually).