Expression tree validation

Question

I am trying to find a practical way (for example, from the point of view of engineering efforts) to solve a problem where I have a bunch of unknown values:

val a: Int32 = ??? val c: Int32 = ??? val d: Bool = ??? 

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

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

I have Boolean operators and or xor not , and 32-bit integers have things like comparison, addition, multiplication, division (NOTE: they must take into account 32-bit overflow!), As well as some bitwise things (shifts, bitwise &, | ^). But I don’t need to support all these operations [See: LOL_NO_IDEA]

And I want to get one of three answers:

• ES_POSSIBLE [I don’t need to know how, just say that it could exist]
• IMPOSSIBLE [No matter what values ​​my variables i.e. this equality will never be true]
• LOL_NO_IDEA [This is acceptable if the problem is too complicated or takes a long time for it]

None of the problems that I solve is too big or complex, with too many terms (most of them are in the order of hundreds). And the presence of a large number of LOL_NO_IDEA is in order. However, I solve millions of these problems, so fixed costs are going to bite (for example, they are converted to text format and cause an external solver)

Since I do this with scala, using SAT4J looks pretty attractive. Although the documentation is terrible (especially someone like me who has just peered into this SAT world for a couple of days)

But my current thinking is to first turn all Int32 into 32 Booleans. That way I can express relationships like (a <b) by doing this as a nested boolean expression (compare msb if they are eq, then next, etc.)

and then, when I have a large tree of Boolean variable expressions and Boolean expressions - to then cross it on a gradual build-up: http://en.wikipedia.org/wiki/Conjunctive_normal_form

and then submit it to SAT4J.

However, it all looks very complicated - and even creating CNF seems very inefficient (making it in a naive way that I implement it) and error prone. Not to mention the attempt to code all Integer math expressions as Boolean expressions. And I could not find good resources intended for someone like me, an engineer with a problem requiring the use of a SAT solution, as basically a black box.

I would be grateful for any feedback, even if he likes "lol, your idiot - look at X" or "yes, your thinking is correct. Enjoy!"

Answer 1

You might want to take a look at Z3 ( http://z3.codeplex.com/ ) or some other crucial modulo theory (SMT) problem. As far as I can tell, the problem you are talking about involves linear integer arithmetic, or possibly bitvectors. I think I would rather have a solver with some understanding of these theories, rather than encode the problem only with Boolean ones.

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

When using the SAT solution, you usually should not enter your problem into CNF yourself. The solver must pre-process your formula (usually using the Zeitin transformation http://en.wikipedia.org/wiki/Tseitin-Transformation ).

Another possibility you could explore is limiting your limits. I know Choco ( http://www.emn.fr/z-info/choco-solver/ ).

Answer 2

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