Naïve question, but doesn't amount of brute-force search depend on the particular solver used? I'm vaguely aware of finite domain something or other but curious about the affordances prolog has for using different solvers over different parts of your codebase.
At first guess, I would imagine this could look like writing down known constraints on the solution as a kind of "type declaration".
Prolog's clpfd (constrained logic programming over finite domains) is actually just a library - albeit one with very ergonomic bindings that mesh almost invisibly into the language.
Prolog's evaluator backtracks when it hits a conflict while trying to expand a predicate. It evaluates queries top-down, and tries predicate definitions/clauses in order. It's basically eager. This isn't a good fit for math, so CLPFD fixed this by making arithmetic constraints lazy. This works really well, but you're ultimately using Prolog to build a model, then (invisibly) solving the model separately.
Ultimately, the problem is that Prolog looks like a DSL but is Turing-complete. You can weave other solvers into the language, but there's a seam between the evaluators. I like the alternative, which is to sacrifice Prolog's Turing-completeness for a ridiculously powerful DSL. Answer Set Programming (clasp) and Datalog are fine examples of this.
Comments
Naïve question, but doesn't amount of brute-force search depend on the particular solver used? I'm vaguely aware of finite domain something or other but curious about the affordances prolog has for using different solvers over different parts of your codebase.
At first guess, I would imagine this could look like writing down known constraints on the solution as a kind of "type declaration".
Prolog's clpfd (constrained logic programming over finite domains) is actually just a library - albeit one with very ergonomic bindings that mesh almost invisibly into the language.
Prolog's evaluator backtracks when it hits a conflict while trying to expand a predicate. It evaluates queries top-down, and tries predicate definitions/clauses in order. It's basically eager. This isn't a good fit for math, so CLPFD fixed this by making arithmetic constraints lazy. This works really well, but you're ultimately using Prolog to build a model, then (invisibly) solving the model separately.
Ultimately, the problem is that Prolog looks like a DSL but is Turing-complete. You can weave other solvers into the language, but there's a seam between the evaluators. I like the alternative, which is to sacrifice Prolog's Turing-completeness for a ridiculously powerful DSL. Answer Set Programming (clasp) and Datalog are fine examples of this.