ai @ wvu
Modeling Intelligence Lab ("the MILL")
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.
1) Read DIMACS model, and run the above routine.
2) Not all the solutions will be useful. What I need is feature-rich solutions.
Post a Comment
Post Comments (Atom)