3 ms·
Don't get me wrong, Prolog is cool... but in 2021, why use a completely different language and not a SAT solver DSL (domain specific language) bound into your f
by asah 5y ago
Don't get me wrong, Prolog is cool... but in 2021, why use a completely different language and not a SAT solver DSL (domain specific language) bound into your favorite imperative language, e.g. Python. Then you get all your favorite libraries for I/O, data transformation, UI/UX, etc.
Examples include Google OR-tools, Microsoft Z3, etc.
https://developers.google.com/optimization https://developers.google.com/optimization
https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3
- maweki 5y agoI understand the sentiment for a problem where the instance size is quite known. SAT solvers have become incredibly fast. Just note that encoding terms of various shapes in SAT is very difficult. Encoding terms of unknown size doubly so. Encoding problems in Prolog is very easy in that sense, as you can build arbitrarily shaped terms very easily and you can constrain variables within terms and not only on the top level. The sudoku example, with the fixed shape and all variables at the top level is a prime example for SAT solving though.