Constraint satisfaction problem: solve system, then evaluate whether many additional constraints are satisfied one at a time

Question

I have a system that consists of binary inequality constraints between variables, plus some indicator variables that can assume only two values:

a, b, c, d ⊆ ℝ
i ⊆ {true, false}

// unconditional inequality constraints
a < b

// conditional inequality constraints
i -> b < c
i -> b < d
!i -> b > c
!i -> a < d

and I would like to answer questions about the system, such as "is a greater than d?" and "is c less than d?".

One approach would be to formulate this as an integer linear program: in the example above, the non-indicator variables would have domains [0, 3], the indicator variables [0, 1] and a feasible solution might be:

i = 0 (false)
a = 0
b = 1
c = 0
d = 2

I could then answer "is a greater than d?" by comparing the integer values assigned to a and d. However, I could get the wrong answer for "is c less than d?": the solution above suggests yes, but there exists another feasible solution

i = 0 (false)
a = 0
b = 3
c = 2
d = 1

in which the answer appears to be no. (The correct answer is that we cannot determine the relationship between c and d.)

Now, I could generate ALL the feasible solutions, iterate over them, and check whether c < d in each one -- but I have to answer enough of these questions that this approach would be too slow.

Is there a more efficient and elegant way? Perhaps constraint programming is not even the right way to think about this -- I considered formulating it as a directed graph-search problem instead, where directed edges represent inequality relationships, but my actual system contains conditional constraints as well. The wonderful answer that I received on a related question (https://scicomp.stackexchange.com/questions/36090/constraint-programming-problem-with-conditional-constraints-and-some-unknown-ind) directed me here. Glad for any suggestions or references to relevant papers or textbooks!

Edit: After asking this question to several people (both here and elsewhere), I have received multiple suggestions to reduce these constraints to a comparability graph. To illustrate the challenges of this approach, I have added conditional constraints to my example system above. Is there a way to incorporate such constraints into a comparability graph?

Answer 1

If the constraints you have are of the form $a < b$ and $a=b$ (i.e., only unconditional inequality constraints), you can model them with a directed graph: each node represents a variable, and an edge $v \to w$ corresponds to the inequality $v < w$. Then you can answer queries by doing a straightforward reachability check. (If you see the equality $v=w$, then merge the two vertices $v,w$ into a single vertex.)

---

When you add conditional equality constraints, the problem becomes NP-hard.

Proof of NP-hardness: I will show a reduction from 3SAT to your problem. Suppose we have a 3SAT formula $\varphi$ on variables $x_1,\dots,x_n$. Consider a single $C_i = \ell_i \lor \ell_j \lor \ell_k$, where $\ell_i,\ell_j,\ell_k$ are three literals (e.g., $\ell_i$ is either $x_i$ or $\neg x_i$, etc.). We will translate this to the constraints $$\begin{align*} \ell_i \implies &y_{i0} > y_{i1}\\ \neg \ell_i \implies &y_{i0} < y_{i1}\\ \ell_j \implies &y_{i1} > y_{i2}\\ \neg \ell_j \implies &y_{i1} < y_{i2}\\ \ell_k \implies &y_{i2} > y_{i3}\\ \neg \ell_k \implies &y_{i2} < y_{i3}\\ \end{align*}$$ $$y_{i0} > y_{i3}$$ Notice that if at least one of $\ell_i,\ell_j,\ell_k$ are true, then these seven constraints are simultaneously satisfiable; but if $\ell_i,\ell_j,\ell_k$ are all false, then they are not satisfiable. So, we translate each clause of $\varphi$ into several constraints as above, obtaining a large system of constraints. Then this system has a satisfiable solution if and only if $\varphi$ is satisfiable.

In conclusion, testing satisfiability of your kind of constraints is NP-hard. It follows that answering queries is also NP-hard (answering a query is the same as testing satisfiability of the constraints plus the query). Consequently, you shouldn't expect any algorithm that is both efficient and always correct.

If you have to solve it in practice, you could try applying a SAT solver. Add boolean variables $s_{b,c}$ to represent $b<c$; then you can translate each constraint into a clause. For instance, $b<c$ translates into $s_{b,c}$, and $i \implies b<c$ translates into $\neg i \lor s_{b,c}$. Finally, add clauses that enforce the consistency of the $s$'s, i.e., $\neg s_{a,b} \lor \neg s_{b,c} \lor s_{a,c}$ for each $a,b,c$. Now answering a query amounts to conjoining the query and testing satisfiability of the resulting SAT formula, which you could do with an off-the-shelf SAT solver. Some SAT solver allow you to "push" a clause, test satisfiability, and then "pop" the clause.

Answer 2

Is there a specific language you must write that in?
If not, then if all you need are questions of type $x = y$? and $x < y$?, I would say Prolog is a safe bet. You could just load your equalities and inequalities as rules and then add a general rule that says that $<$ and $=$ relations are transitive and $=$ is also reflexive and then you could ask a question like "Is it true that $b > c$?"