Impact of input order on performance of constraint solver

Question

Does the input ( boolean and arithmetic equations ) order matters to the constraint solvers like Gecode and SMT solvers like microsoft Z3 ?? If yes, which one of these two will perform better provided that I can take advantage of some pre-known heuristics using branching function in Gecode ??

(Note : I dont know if function similar to branch() in Gecode, exists in Z3)

Answer 1

In theory, no; order should not matter. The order of assertions should not make a difference. But in practice, they can have an impact as heuristics might end up spending a lot of time in dead-ends. SMT solvers usually work as black-boxes, i.e., it's hard to see how they are progressing unless you know their exact internals. You can, however, turn up verbosity (use z3's -v flag) and might look at the output to see if you spot any divergent behavior.

As with any general "performance of SMT solver" question, it is impossible to answer in the abstract. Each problem instance has specific characteristics, and there might be different ways of coding it to make it easier for the solver. If you post specific problems, you can get better suggestions.