Satisfiability with relational operators instead of boolean variables
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.