CODEWITHSUNDEEP
z3smtz3py
Yang Zhao
Yang Zhao

Reputation: 325

Reasoning based on partial assignments of variables in an SMT problem

I have a simple scenario and see if Z3 could help me: assume there are a set of contraints and can be converted to an initial SMT problem to check satisfiability. I could get values of the variables shown in this SMT problem step by step, and I want to check after each step whether it could have concluded the sat/unsat result. Example:

a = Int('a')
b = Int('b')
c = Int('c')
s = Solver()
s.add(And(a>5, b<7, c>10))

And(a>5, b<7, c>10) is the original problem. Then I get a == 6. The problem could be simplified as: And(b<7, c>10). Then I get b==7, now the problem is unsat, even without knowing the value of c.

Is there a way that solver could show everytime after we get an assignment on a variable whether the current problem is sat/unsat now, and even better, simplify and show the current constraint?

More background: this process is to mimic how we find true or false answer to a complicated condition. All variables in fact have values, but those values are discovered variable by variable, step by step.

Simple example: the requirement to a benefit is: 18 years older and yearly incoming less than Y. In our brain, we will first check our age, if less than 18, the process stop as false/unsat. Else, we could go on checking our incoming.

After we get values to all variables, the condition must evaluate to a true/false answer so the process would always terminate. However, the process could stop earlier if the condition could evaluate even some values of variables are unknown.

Upvotes: 0

Views: 54

Answers (2)

alias
alias

Reputation: 30525

There's a couple of different threads here. The first one is whether Z3 can simplify expressions, based on the constants it found in particular. It indeed can. But as you observed with your call to simplify what z3 considers simplified and what a "human" would consider simplified do not necessarily match. You can find many questions on StackOverflow asking for similar features. My opinion is that relying z3's simplify for human presentation is a futile effort: The tool will simplify to make the goals "simpler" for its own internal purposes. And those purposes hardly ever match what you'd consider "aesthetically pleasing." That's just not what the simplifier is for.

Regarding using partial-assignments, you can do that in SMT solvers with ease. They all allow incremental solving, i.e., you can inspect values and assert new facts as you proceed. The details of this is entirely problem specific of course, but here's an example that sort of models what you described:

from z3 import *

a = Int('a')
b = Int('b')
c = Int('c')
s = Solver()

s.add(And(a>5, b<7, c>10))

def checkAndGetVal(v):
    r = s.check()
    if r == sat:
        m = s.model()
        return m[v]
    else:
        print(f"Solver said: {r}")
        exit

av = checkAndGetVal(a)
print(f"a is {av}")

# Commit to this choice:
s.add(a == av)

# After programming, you decided b is 7, somehow. OK, let's assert:
s.add(b == 7)
checkAndGetVal(b)

This prints:

a is 6
Solver said: unsat

You can also push/pop contexts; i.e., you can push a new context, make decisions (i.e., s.add) and explore a particular path, and than pop back to the point you pushed and explore some other path.

Stack-overflow works the best if you are very specific with your question, as opposed to general questions; however. If you get stuck, I'd strongly recommend posting actual code-segments on what you tried and what didn't quite work like you expected. That allows readers to experiment with your code and suggest alternatives better.

Upvotes: 0

Mohamed Rafiq
Mohamed Rafiq

Reputation: 1

Yes, Z3 can help you achieve this. You can use the check() method to check satisfiability and the simplify() function to simplify constraints after each assignment.

Upvotes: 0

Related Questions