[Question] The fastest way to evaluate a constraint

[Hanseltu]

Hi there,

May I ask what could be the fastest way to evaluate a constraint? The scenario I encountered is that, assuming I have a constraint (say C) and a concrete value (say 100) of a symbol (say a) in C, and I want to evaluate whether the concrete value 100 of the symbol a could make the constraint C true or false, i.e., sat or unsat.

Currently, my solution (using C++ APIs) is to encode the constraint a == 100 into C and invoke solver.check() to check the satisfiability of the new constraint C && (a == 100). Such a solution can work as intended but I found it's pretty slow---every time it needs to invoke check() to evaluate it. I have tried to find a faster way to do the evaluation but failed. Are there any other solutions that could make this evaluation faster, e.g., the one without calling the solver.check()?

Thanks and look forward to your suggestions.

Best regards, Haoxin

[nunoplopes]

There's no way around calling check() for each concrete value. Unless you're lucky. For example, you can try to get a model just for C. If a is not in the model, then it's SAT for any a.

If you know a priori all the concrete values you care about, you can do: C && (a == 1 || a == 2 || ... ).

Then get a model. It has a=2, for example.

Then assert on the same solver a != 2.

Continue until it's unsat. You'll do n+1 queries, where n is the number of concrete values of a for which the formula is SAT. Plus, you'll be doing incremental solving without push/pop (that is slow).