Tuesday, June 18, 2013

How to enumerate solutions using Z3


1) Find first solution, record it
2) Rerun SAT blocking the previous solution, find one more solution, record it
3) Rerun SAT blocking the first 2 solutions, and so forth.

Strange that SAT has to be repeated all over again each time. This is why enumeration takes time.

Need to:
1) Read DIMACS model, and run the above routine.
2) Not all the solutions will be useful. What I need is feature-rich solutions.

No comments:

Post a Comment