It has bindings for other languages and is able to make some rather sophisticated arithmetical and logical deductions in an often pretty efficient way. I've used it successfully for parts of puzzle competitions and CTFs (and I'm really only beginning to scratch the surface of what it can do).
You can read more about the options in that area at
These systems can feel pretty magical and are getting more powerful all the time. (Of course there are cases where there is a better algorithm that you could find, perhaps a much more efficient one, and using these solvers will be asymptotically or worst-case slower than it had to be given more human insight.)
Some of these could be overkill for your application, and Z3 doesn't have a Javascript binding, so I guess it's not as helpful for web forms.
Do you have any suggestions on how to get started? I remember reading "The unreasonable effectiveness of SAT solvers" or whatever it was called which showed that SAT solvers are not always the most efficient performers, but they can take you within a factor 10 in much less time. I remember thinking, "Oh, but what about SMT solvers, then?" But not getting anywhere with that.
SAT, SMT, constraint programming lie on a continuum. SMT is SAT plus machinery from constraint programming. I'm not an expert on this, just info from this video. According to him constraint programming will win in the long run because of constraint programming has larger structures which can be exploited with global constraints (SAT is only a flat sequence).
https://github.com/Z3Prover/z3
It has bindings for other languages and is able to make some rather sophisticated arithmetical and logical deductions in an often pretty efficient way. I've used it successfully for parts of puzzle competitions and CTFs (and I'm really only beginning to scratch the surface of what it can do).
You can read more about the options in that area at
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
which also links to the related tools in
https://en.wikipedia.org/wiki/Answer_set_programming
https://en.wikipedia.org/wiki/Constraint_programming
These systems can feel pretty magical and are getting more powerful all the time. (Of course there are cases where there is a better algorithm that you could find, perhaps a much more efficient one, and using these solvers will be asymptotically or worst-case slower than it had to be given more human insight.)
Some of these could be overkill for your application, and Z3 doesn't have a Javascript binding, so I guess it's not as helpful for web forms.