0

I am trying to use Z3 (SMT solver) to verify and rank a list of solutions. In verification system,I have some constraints and evaluation criteria and based on that I wanted to rank the solution using SMT solver. My question is, can Z3-SMT solver rank the list of solution based on some criteria as in my limited understanding SMT solver are Boolean? I am not only interested in yes/no solution but rank the solution based on solver. Any literature source for this kind of situation can be helpful, as I am from another domain.

Edit: Ranking can be thought as score to different solution. For example, lets assume we have 2 solution and both are feasible but among them I want to select only 1 solution. To do that I am thinking to use Solver to assign some kind of score to solution, so that among multiple feasible solution I can select best solution based on score. Its like ranking of students in classroom.

2
  • What’s the “rank” of a solution? I’m afraid this isn’t common terminology. You’ll have to explain us what you mean by ranking a solution, hopefully with a simple example.
    – alias
    Dec 12, 2022 at 3:45
  • thanks for pointing it out. Based on your comments, I have edited my question.
    – Rambo_john
    Dec 12, 2022 at 7:45

1 Answer 1

1

It's impossible to opine without exactly knowing what this "ranking" precisely involves. Assuming it's some sort of a "cost function" associated with each solution, you can ask an optimizing SMT solver to minimize/maximize that cost function. So, if you can express this "ranking" as a numeric value associated with a solution, you can ask z3 to return a solution that has the maximum (or minimum) such value. Note that z3 can only optimize linear functions; so if your "ranking" involves any sort of non-linearity, it won't work.

For details see: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-optimization

Aside from z3, MathSAT can also do optimization as well, using a different approach: https://optimathsat.disi.unitn.it. Might be worth a try if z3 doesn't perform well.

1
  • thanks, I was also thinking in the line of cost function. As in my case ranking is similar to neural network classification where model output probability and highest SoftMax value is taken as correct class but in my case lower rank solution is also correct unlike typical classification which are either this option is right else is false.
    – Rambo_john
    Dec 12, 2022 at 20:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.