1
$\begingroup$

My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to solve constraints across multiple theories, as with SMT solvers. To demonstrate, I have created a set of constraints using (I think) the theories of strings, arrays, integers, real numbers, bit vectors, and (I just made it up) files. Here are the variables:

x: a string variable
y: a string variable
a: an array variable
b: an array variable
i: an integer variable
j: an integer variable
m: a real number variable
n: a real number variable
v: a bitvector variable
w: a bitvector variable
p: a file variable
q: a file variable
r: a boolean variable
s: a boolean variable

And here are the constraints:

exists(x) && exists(y)      // String theory + Existence theory?.
  && length(v) > length(w)  // Bitvector theory.
  && length(x) != length(y) // String theory.
  && i > j                  // Integer theory.
  && m > n                  // Real number theory.
  && r || s                 // Boolean theory.
  && read(p) != read(q)     // File theory.
  && a[i] != a[j]           // Array theory.
  && a[i] != i              // Array theory mixed with integer theory.
  && m != i                 // Real number theory mixed with integer theory.
  && j > length(x)          // Integer theory mixed with string theory.
  && match(read(p), y)      // String theory mixed with file theory.
  ...

First question is if I am conceptualizing this correctly. I don't know if I am using the word "theory" in the list of constraints properly. For example, "Array theory mixed with integer theory", wondering if that example is correct.

The main question is the general way to go about solving this problem. I assume this is an SMT problem, since it involves more than just Boolean variables. Wondering if I somehow break this apart, normalize it into CNF, or otherwise divide it into pieces that can be solved independently. And then how to integrate the solutions. The reason I ask this part of the question is because I have seen the Nelson Oppen method suggesting how to combine theories (but I am not that far in my understanding yet). I am still trying to get a grasp of how to translate common programming constraints (like what I demonstrated above) into something acceptable to an SMT solver.

I am not asking about how to actually solve this problem, because from my understanding so far, each theory would require its own complex set of decision procedures (algorithms). I am just wondering what the general steps are for solving this problem of:

How to find values for $x$, $y$, $a$, $b$, $i$, $j$, $m$, $n$, $v$, $w$, $p$, $q$, $r$, $s$ such that the constraint system is satisfied.

I sort of understand how the DPLL algorithm works, but this implies I have all my variables ready for a SAT solver (i.e. in Boolean form), which these variables clearly aren't. So I'm not sure if I should do some preprocessing step to get them into boolean form, or something entirely different.

I am basically looking for a set of steps outlining the process for solving the problem, so I know where to direct where I look. Something like:

  1. Divide the variables into disjoint sets by theory.
  2. Solve each theory independently. The goal is to output a boolean variable for each chunk in the theory.
  3. Combine the theories into a single set of Boolean clauses.
  4. Apply a SAT solver algorithm such as DPLL or CDCL to the Boolean clauses to get the variable valuations that satisfy the constraints.

(That is basically what my understanding is, which is clearly missing some pieces and is misdirected in other parts). But a list of some sort like that is all I am looking for to help guide search.

$\endgroup$
  • $\begingroup$ The boolean variables of the formula given to the SAT-solver are not your original real / vector variables, they are "frozen" atomic formulas (i.e. $P(t_1,\dots ,t_n)$ for $P$ some $n$-ary predicate). For example, for $x=y\land y = z \land\lnot (x=z)$, the SAT-solver could give the valuation $[x=y]\mapsto 1,[y=z]\mapsto 1, [x=z]\mapsto 0$, which would then be given to the theory solver. The theory solver would give an additional constraint to tell the SAT-solver that this solution does not work: $x=y\land y=z\implies x = z$, and then the SAT-solver would search for another solution and so on. $\endgroup$ – xavierm02 Jul 22 '18 at 21:55
  • $\begingroup$ If $x$ and $y$ are strings, they can't be clauses in your constraint formula $\endgroup$ – Curtis F Jul 23 '18 at 14:44
  • $\begingroup$ Updated to fix I think what you were saying. $\endgroup$ – Lance Pollard Jul 23 '18 at 16:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.