1
$\begingroup$

I have a large number of equivalences which look like:

$(a \leq 0.54 \wedge b \geq 0.12) \vee (c \gt 0.98)$ $\Leftrightarrow$ $(x \leq 0.25) \vee (x \gt 0.91 \wedge y \geq 0.01)$

This is just an example. In general, formulae on either left or right side of the equivalence could be anything that takes the form of a disjunctive normal form (DNF) clause, the numbers could be any real numbers with a fixed precision, and the inequality signs could be $\leq$, $\lt$, $\geq$, or $\gt$.

What is important is that the possible variables on the left side of all the formulae (here $\{a, b, c\}$) form a set that is distinct from the possible variables on the right side of all the formulae (here $\{x, y, z\}$). There could be any fixed number of variables on either side: doesn't need to be 3 variables, and doesn't need to be an equal number on either side.

I also have some implications of the form:

$(a \leq 0.32 \wedge b \geq 0.62)$ $\Rightarrow$ $(c \gt 0.00)$

Here both left and right sides are just conjunctions of inequalities, but what is important is that the set of variables on both left and right sides, i.e. $\{a, b, c\}$ here, is the same as the set of variables on only the left side of the previous kind of the formula (i.e. the equivalences).

My question is: what kind of automated reasoner would I need to find the logical consequences of a set of such formulae? I am just looking for a concrete identification of the general class of problems this belongs to, and any out-of-the-box reasoners which may be available. Perhaps this is an SMT problem?

$\endgroup$
4
  • $\begingroup$ The condition on variables on sides is irrelevant. There is no need to explain it so much. On the other hand the part when you say "formulae on either left or right side could be anything" does need to be explained. It can change the problem from decidable to undecidable. $\endgroup$ – plop Aug 27 '20 at 12:59
  • $\begingroup$ Thanks. I said "formulae on either left or right side could be anything takes the form of a disjunctive normal form (DNF) clause", meaning any disjunction of conjunctions, but each "variable" x being of the form x less than/more than some real number, instead of being a propositional variable which is either 0 or 1. I just noted the superficial similarity to a DNF formula. $\endgroup$ – Velvet Ghost Aug 27 '20 at 13:47
  • $\begingroup$ I see now. By left and right you are referring to the equivalence, not to the inequalities. $\endgroup$ – plop Aug 27 '20 at 14:25
  • $\begingroup$ Yes, I mean the left and right hand sides of the <=> or =>. Sorry for the confusion. $\endgroup$ – Velvet Ghost Aug 27 '20 at 14:26
2
$\begingroup$

Yes, you could solve this with a SMT solver that supports linear real arithmetic. However SMT supports more general inequalities where you can have linear sums of variables (e.g., $2a+3x \le 5.7$) instead of simple comparisons between a single variable and a constant (e.g., $a \le 1.6$), so it might be more powerful than you need, so if you don't have any linear inequalities involving sums, then I agree with Pseudonym that the best approach may be to use a SAT solver.

I would suggest a slightly different encoding to SAT. Instead of a one-hot encoding, where $x_i$ means that $c_{i-1} \le x \le c_i$, I would suggest a slightly different encoding: $x_i$ means $x \le c_i$. Thus instead of encoding to a $(x_1,\dots,x_n)$ vector like $(0,0,0,1,0)$ you would encode to $(1,1,1,1,0)$. You add constraints that $x_i \implies x_{i-1}$, and then each inequality $x \le c_i$ corresponds to a boolean variable $x_i$.

$\endgroup$
2
  • $\begingroup$ This is also not a bad idea. The one thing I'd add is that you may need to take care with equality; $x \le 0.5$ vs $x < 0.5$. $\endgroup$ – Pseudonym Aug 28 '20 at 3:32
  • $\begingroup$ I'm accepting this answer because it pointed out that an SMT solver supporting LRA can tackle this problem. This was easier for me than encoding in SAT; I used Microsoft Z3. I also found out from Z3's documentation that this is or is very similar to a simplex problem, and Z3 in fact uses a dual-simplex solver for it, "under the hood". $\endgroup$ – Velvet Ghost Sep 17 '20 at 16:07
3
$\begingroup$

In your case, the simplest solution may be to use SAT.

Your first clause includes $x \le 0.25$ and $x > 0.91$. This means that there are five regions of interest for the variable $x$, which we identify with boolean variables: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in (0.91,\infty)$.

Create a boolean variable for each of these ranges, and convert the clause to use them. So, for example, $x \le 0.25$ would convert to $X_1 \vee X_2$, and $x < 0.91$ would convert to $X_1 \vee X_2 \vee X_3$.

More clauses would mean more constants, and hence more ranges of interest for a primitive variable.

$\endgroup$
3
  • 1
    $\begingroup$ Thanks. This is a very useful insight. Is this (constructing propositional variables from ranges of real numbers and then using a SAT solver) a known/established technique with existing software tools? Upon searching, I couldn't find anything similar. $\endgroup$ – Velvet Ghost Aug 27 '20 at 15:06
  • 1
    $\begingroup$ @VelvetGhost, yes, it's standard (at least it's something I've heard of before). It's just that it often can't be used. $\endgroup$ – D.W. Aug 27 '20 at 23:58
  • 1
    $\begingroup$ I've never seen it before, but I defer to D.W. on this one; it seems like the sort of thing that someone else would already have thought about. The way I came up with it was I thought of cylindrical algebraic decomposition, and then realised that it's a trivial case of that. $\endgroup$ – Pseudonym Aug 28 '20 at 3:07

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.