4

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!"

ziggystar
  • 28,410
  • 9
  • 72
  • 124
Heptic
  • 3,076
  • 4
  • 30
  • 51

2 Answers2

6

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/).

Matthias Schlaipfer
  • 510
  • 1
  • 3
  • 15
  • Awesome! I've been reading through your links, and your advise is making a lot of sense. I'll leave the question open a big longer, incase anyone else has some other useful tips – Heptic Apr 07 '13 at 17:57
  • Just even the mention of Tseitin-Transformation has been immensely useful. It's put me on a much better path, thanks! – Heptic Apr 07 '13 at 18:16
  • I'm glad I could help. Most of my knowledge is of theoretical nature, but feel free to ask if there is anything else. I'll do my best to help. – Matthias Schlaipfer Apr 07 '13 at 18:29
  • Very good answer. And thanks for pointing me to the Tseitsin-Transformation, too. – ziggystar Apr 08 '13 at 08:14
1

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.

Daniel Le Berre
  • 11
  • 1
  • This looks really great! I'm either going to use it, or at least use it heavily for reference =) – Heptic Apr 08 '13 at 15:45
  • Do you know how efficient using something like this, where all my ints are like: int('x, INT.MIN, INT.MAX) ? Is that going to cause it to explode, and I should instead manually explode it into booleans? Or it should be fine? – Heptic Apr 08 '13 at 15:52
  • well, it will explode for sure. Usually model checking is performed with a bounded length for ints (a tool like Alloy http://alloy.mit.edu/ uses by default ints on only 4 bits…) If you really need to manipulate full ints, you should go the SMT way. – Daniel Le Berre Apr 08 '13 at 18:26