Question on optimizing the running time

Sep 20, 2013 at 5:21 AM

I am using Z3 to determine shortest paths in a graph. Somehow, Z3 takes around 1 min 38 secs to find the shortest path, but around 2 min 58 seconds to find "any path irrespective of cost". Could somebody through some light on why a seemingly easier problem is taking almost twice the time?
Sep 20, 2013 at 12:01 PM
Without looking at the actual problem you are feeding into Z3, this question is nigh impossible to answer. It could a multitude of things; in the extreme case it could be that the heuristics get lucky on one problem and unlucky on the other. It may also depend heavily on your encoding of the graph and the properties. Could you perhaps share your input files so we can take a closer look?