CODEWITHSUNDEEP
javaz3smtsat
Prashant Kumar Singh
Prashant Kumar Singh

Reputation: 193

Microsoft Z3 get relevant assignments

How do I get only the relevant value assignments for the variables used after the z3 satisfiability check?

For example:

I have multiple assertions that are given as constraints to Z3 Sat Solver, whereas a single Boolean Expression that I need to check for whether it satisfies or not.


Note: The assertion may contain variables which are not present/irrelevant in the Boolean Expression (Formula)

The values assigned to the model contain the assignment for the assertion constraints as well which has no impact on the satisfiability of the Boolean Expression.

I can see in the module smt.relevance: 2 as default value in z3 configuration.
How do I limit it only to the variables which have an impact on the Expression satisfiability?

Upvotes: 0

Views: 206

Answers (1)

alias
alias

Reputation: 30525

You cannot do this, in general. A SAT solver will "heuristically" solve the constraints to find a satisfying assignment, and in general, you cannot control how that search proceeds. They do not find any sort of "minimal satisfying assignment."

You can restrict the output to contain only those variables that occur in the formula, and query for the values of those at the end. If your formula has a variable whose assignment is irrelevant to SAT, this technique will obviously not work, but it should get you far.

Upvotes: 0

Related Questions