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:

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.

• – Yuval Filmus Dec 22 '17 at 23:16
• Thanks @YuvalFilmus. I just found out that sub field after posting this too. The linear arithmetic SMT's seems to be what I'm looking for, though it seems to be pretty complex and not ported to web languages yet ; ). I'm not sure if it's worth the time to really dive in if my goal is a (simple'ish) implementation in javascript for query optimization. Anyone an idea what algorithms I can look at without having to dive too deep? – jasper Dec 23 '17 at 0:20