Automated reasoning with real numbers

Question

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?

Answer 1

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$.

Answer 2

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.