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 a 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 are 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 equasion 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 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

You might want to take a look at Z3 (http://z3.codeplex.com/), or some other satisfiability modulo theories (SMT) solver. The problem you're stating involves linear integer arithmetic or possibly bitvectors, as far as i can tell. I think I would prefer having a solver with some understanding of these theories rather than encoding the problem with just Booleans.

Z3 has Java bindings (see http://research.microsoft.com/en-us/um/people/leonardo/blog/2012/12/10/z3-for-java.html). I haven't used them myself, though, and am not sure how much overhead there is.

When using a SAT solver you typically don't have to put your problem into CNF yourself. The solver should preprocess your formula (usually by means of the Tseitin transformation http://en.wikipedia.org/wiki/Tseitin-Transformation).

Another option you could look into is constraint satisfaction. I know of Choco (http://www.emn.fr/z-info/choco-solver/).

Answer 2

Since you are a scala programmer, you might want to use directly a scala library such as Scarab http://kix.istc.kobe-u.ac.jp/~soh/scarab/ Such tool offers you a modeling of the problem in Scala with a resolution of the problem with a SAT solver.