Is z3 the most efficient solver for quantifier-free integer propositional logic? [closed]

Question

Sorry that this question is subjective, but given that the Stack Overflow has the largest Z3 user base, I want to give it a try.

I have a big constraint satisfaction problem that consists of many integer propositional logic formulas and a few first order logic formulas that only contain integers(quantifiers). I care very much about the efficiency, because I am building an interactive program synthesizer.

I am now using z3 solver and the check time is sometimes too long. I wonder if z3 is the best tool to tackle the problem I mentioned in above or there is a better tool? How about CPLEX?

Any suggestion will be appreciated.

Edit:

Sorry, the code has been remove for privacy reason. I can email you my code personally if you are willing to take a look. Thanks in advance.

Pinnate

Please post an example of the problem that currently takes too long with Z3, so we can compare alternatives for your use case. – Dudden

did you tried quacode ? – Mindi

@Dudden I just posted my code. Thanks. – Pinnate

You sure you are seeking quantifier free "integers" solver. Strictly speaking a solver that says yes or no always, doesn't exists. en.wikipedia.org/wiki/… If you were fine with bounded domains you could try CLP(FD) as well. – Bambibambie

In my experience, z3 performs better than Gurobi (the ILP solver) in my big Integer Linear Problem. You can see the slightly better performance of gurobi vs CPLEX in their own report like gurobi.com/pdfs/benchmarks.pdf . The users mostly believe that Gurobi and CPLEX show same performance. Therefore, I think Z3 would be better than CPLEX too. – Allaround