Checking satisfiability of expression tree

Question

I'm trying to look for a practical way (e.g. in terms of engineering effort) of solving a problem, where I have a bunch of unknown values:

val a: Int32 = ???

val c: Int32 = ???

val d: Bool = ???

and an expression binary-tree (in memory), that ultimately returns a boolean, e.g.

((a > 4) || (b == (c+2))) && (a < b) && ((2*d)) || e

The boolean operators I have been and or xor not and the 32-bit integers have stuff like comparison, as well as addition, multiplication, division (NOTE: these must respect 32-bit overflow!) as well as some bitwise stuff (shifts, bitwise &, | ^ ). But, I don't need to necessarily support all those operations [See: LOL_NO_IDEA ]

And I want to get one of three answers:

• ES_POSSIBLE [I don't need know-how, just be told that there exists a way it could be]
• UNPOSSIBLE [No matter what values my variables hold, this equation would never be True]
• LOL_NO_IDEA [This is acceptable if the problem is too complex or time-consuming for it]

None of the problems I'm solving are overly large, or complex, with too many terms (The most is in the order of hundreds). And having a large amount of LOL_NO_IDEA's are fine. I am however solving millions of these problems, so constant costs are going to sting (e.g. transforming into text format, and evoking an external solver)

Since I'm doing this from scala, using SAT4J looks quite appealing. Although, the documentation is horrible (Especially someone like me, who's only looked into this SAT world for a couple of days)

But my current thinking is to first turn all each Int32 into 32 booleans. That way I can express relationships like (a < b) by doing it as nested boolean expression (compare the MSB, if they're eq, then the next, etc. )

and then when I have a big expression tree of boolean variables and boolean expressions -- to then traverse it while incrementally building up a: http://en.wikipedia.org/wiki/Conjunctive_normal_form

and then feeding that into SAT4J.

However, all this looks very challenging -- and even building up CNF seems very inefficient (doing it the naive way, that I'd implement it) and error-prone. Let alone trying to encode all the Integer maths as boolean expressions. And I haven't been able to find and good resources designed for someone like me, an engineer with a problem wanting to use SAT solving as largely a black box

I'd appreciate any feedback, even if it's like "lol, your an idiot -- look at X" or "yeah, your thinking is right. Enjoy!"

Answer 1

The problem you're stating involves linear integer arithmetic or possibly bit-vectors, as far as I can tell. I would favor having a solver with some understanding of these theories rather than encoding the problem with just Booleans.

Refer to the following link, for more information regarding Z3 which is a satisfiability modulo theories (SMT), solver: https://github.com/Z3Prover/z3

If you are looking to learn more about Artificial Intelligence then you visit Artificial Intelligence Tutorial and Artificial Intelligence Course. Also, if you are appearing for job profiles of AI Engineer or AI Expert then you can prepare for the interviews on Artificial Intelligence Interview Questions.