Satisfiability with relational operators instead of boolean variables

Question

Question

What is the state of the art for relation/equality satisfiability problems and where can I find papers clearly describing algorithms used (Or even better: implementations of them. Or even better: javascript implementations - I know that's a long shot)?

I.e. How do I solve satisfiability of: x > 10 && y < 5 && x < y

Long introduction

boolean satisfiability

The boolean satisfiability problem is quite well documented. However I cannot find algorithms for cases when propositions are relational operators rather than booleans.

For example:

To find out if a sentence like p && !p has any values of p for which it is true, is well documented and ready-made algorithms exist. Often the sentence is transformed to Conjunctive Normal Form (CNF) and then a CNF-SAT solver is used. For example:

• http://logictools.org/index.html

relational/equality satisfiability

However I cannot find algorithms for cases when propositions are relational operators rather than booleans. Think of a statement like x > 10 && !(x < 5) or x > 10 && y < 5 && x < y. This seems a way less studied problem.

For example: Transforming equality logic to propositional logic is very theoretical, I couldn't really understand it and thus use it for implementation.

Solving Satisfiability and Implication Problems in Database Systems actually lead me to a solution. It explains how to solve satisfiability for sentences with only conjunctions. Knowing that, I can transform any sentence to Disjunctive Normal Form (DNF) and apply the algorithm to each conjunction in the DNF. If one of the conjunctions is satisfiable, the whole sentence is.

However, it seems that this is not the most efficient way to solve it. First, this paper is from 1996 and I expect the field to have progressed. Second, converting to DNF is exponentially complex while converting to a equisatisfiable CNF can be done in polynomial time. Most boolean satisfiability solvers seem to convert to CNF and then solve using heavily studied algorithms. It seems a similar approach would be preferable for relational satisfiability.

So my question is: What is the state of the art for relation/equality satisfiability problems and where can I find papers clearly describing algorithms used (Or even better: implementations of them. Or even better: javascript implementations - I know that's a long shot)

I have searched for 2 days in different fields such as SQL query optimizers (contradiction/tautology detection) and theoretical CS but haven't been able to find anything else than the above DNF solution.

Answer 1

Congratulations, you have invented Satisfiability Modulo Theories, also known as SMT. This is a large field of research, and deals with exactly the problem of satisfiability with not just boolean variables, but predicates over some existing logical theories, such as linear integer arithmetic, uninterpreted functions, arrays, etc.

The basic idea is that you alternate between calling a SAT solver and a theory solver. You take your relational formula, and replace every relational statement with a boolean variable, then get a solution from a SAT solver. This gives you a True or False value for each relational statement. You then plug those into your theory solver, which determines if there's a solution that is consistent with the truth value for each relational proposition.

If the solution is valid, then you are done. If it is not valid, then you add the negation of the assignment (or a reduced form) to your original boolean problem, since you know it can't hold, and you repeat until you either the theory solver succeeds or the SAT solver fails.

SMT research doesn't care a ton about theoretical complexity, since everything is NP-hard in the best case, and possibly much worse, depending on your theory. Instead, modern SMT solvers are heavily optimized with heuristics and prunings that allow them to be reasonably fast for common cases.

The two most common SMT solvers are Z3 and CVC4, but I have no clue if either work in JavaScript. Writing an inefficient SMT solver yourself is not too hard, especially if you can use an off-the-shelf SAT solver.