clpz VS core.logic

As pointed out in the comments in the article, these kinds of logic puzzles are easier to solve using constraint programming than "regular" logic programming.

For example, see the solution to the Zebra Puzzle here: https://www.metalevel.at/prolog/puzzles which uses CLPZ[^1].

[^1]: https://github.com/triska/clpz

Scryer has the strings-as-lists-but-implemented-efficiently thing, possibly more strict ISO Prolog compatible syntax, and it may ship with a more advanced constraint library (I'm not clear on the relationship between SWI's clpfd and Scryer clpz).

None of these are full-fledged programming languages, however. They're limited to problems that lie in the polynomial hierarchy (A class which contains P and NP). Logic programming is generally only used to solve hard problems for which no good algorithm is known. Prolog also sort of fits this niche and it has a bunch of solvers integrated into it. Notably CLPFD which uses https://github.com/triska/clpz for constraint logic programming. Rosette (https://docs.racket-lang.org/rosette-guide/index.html) is another solver-based language. Except it uses lisp syntax (it's embedded in the Racket language). It uses Z3 as a solver (linked above for SMT theories)

Constraint programming I guess is when one uses a prolog library such as: https://github.com/triska/clpz

It's also available in Clojure: https://github.com/clojure/core.logic

If you want to write one yourself, it's pretty easy: https://www.youtube.com/watch?v=y1bVJOAfhKY

Something like Clojure's core.logic would be pretty nice too. As I understand it, this is one of those features that has been re-invented time and again in the Lisp world over the years. Although the CL standard is already fairly large, it would probably be a bit controversial to make that a required part of a CL implementation. Still, it would be cool to have the option of using dependent types in the macro system to generate formerly verified Lisp code at compile time.

It also has core.logic which is minikanren. There are other logic programming options as well. Some libraries like core.typed use core.logic for the type checker.

You could study core.logic: https://github.com/clojure/core.logic/tree/master/src/main/c...

I swear I'd bookmarked a resource that was more analogous to #2, but you may want to have a look at The Little Prover: https://mitpress.mit.edu/books/little-prover

related:

https://github.com/clojure/core.logic/wiki/A-Core.logic-Prim...