3
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Check out en.wikipedia.org/wiki/Satisfiability_modulo_theories. $\endgroup$ – Yuval Filmus Dec 22 '17 at 23:16
  • $\begingroup$ 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? $\endgroup$ – jasper Dec 23 '17 at 0:20
2
$\begingroup$

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.

$\endgroup$

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.