Why can small modifications in the input formula produce significant runtime differences?
Z3 can be used to solve many intractable problems (from NP-complete to undecidable). So, it is heavily based on heuristics. For example, let us consider the satisfiability of propositional formulas. You can pass propositional formulas where Z3 can immediately identify a satisfying assignment because the search happened to initially choose the right assignments, or Z3 may be able to identify a small proof quickly because it performed the right case splits early. But if Z3 does not start with the right assignments or case splits it is possible that search may take a long time. The input format influences the initial assignments and case split order.
Related Questions
- How is the workload generated by patients without significant morbidity who believe themselves to be ill recognised in the Carr-Hill formula?
- The costs of accreditation and of required Performance Testing (PT) are significant for small laboratories. Is there any relief in sight?
- What is the reason for significant differences in runtime when identical database accesses are executed?
