CODEWITHSUNDEEP
z3boolean-logicsolverboolean-expressionsmt
moh robati
moh robati

Reputation: 1

Synthesizing a boolean expression based on several constraints

What I need is pretty straight-forward, I'm looking for a tool/library that gets several constraints in a format like this:

  1. {"vars": {a=2, b=1, c=3}, "eval": "False"}
  2. {"vars": {a=1, b=1, c=2}, "eval": "True"}
  3. {"vars": {a=1, b=2, c=1}, "eval": "True"}

And then synthesize a boolean expression for me based on predefined symbols:

I need only one solution for this system; for instance, one can be

I've been looking into Z3 library features but couldn't find anything useful. Please do inform me if you know about an appropriate tool.

Upvotes: 0

Views: 240

Answers (1)

alias
alias

Reputation: 30428

Program synthesis is a very active area of research; and the quality of the programs you'll get really depends on what sort of program templates you want to use. An SMT solver will most likely not give you the kind of programs that you're looking for out-of-the-box, although they will work.

Here's how I'd code your current problem: I'd use an uninterpreted function and add the "test-cases" as constraints. Like this:

(declare-fun f (Int Int Int) Bool)
(assert (not (f 2 1 3)))
(assert      (f 1 1 2))
(assert      (f 1 2 1))

(check-sat)
(get-model)

When I run this, z3 says:

sat
(
  (define-fun f ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    (ite (and (= x!0 2) (= x!1 1) (= x!2 3)) false
      true))
)

If you read the output, you'll see that it essentially synthesized the following program:

   if (a == 2) && (b == 1) && (c == 3)
   then False
   else True

Is this correct? Absolutely. Is this really what you wanted it to do? Most likely not. But out-of-the box you'll not get anything better from an SMT solver.

For synthesizing cool programs using SMT based technologies, see, for instance, Emina Torlak's research. Here's a good paper to start with: http://synapse.uwplse.org

Upvotes: 1

Related Questions