|
|
|
|
|
|
by mjn
4100 days ago
|
|
|
Fwiw some of the later logic-programming work coming out of Prolog has produced languages with Prolog-like syntax but without statement order being significant, and guaranteed termination. This paradigm, Answer Set Programming (ASP), is also based on solvers, so has some relationship to SMT, but feels more like Prolog to program, e.g. it has negation-as-failure. My favorite implementation is from the University of Potsdam [1]. Imo it's a much nicer modeling language, especially for incremental formalization, in part because of implementing a nonmonotonic rather than classical logic. It also has a nice generative-programming style where you can define generative spaces via "choice rules", where the solver is explicitly given a free choice for some variables, subject to constraints, and returns a satisfying artifact/model. That allows using it to construct constrained generative systems (e.g. generative music [2], level generation [3]). But Z3 far outperforms ASP solvers on problems where variables range over large domains (like "32-bit integer") because of the MT part of SMT. There's some experimental work on trying to combine the approaches, using Z3 (or another SMT solver) as the solver backend for a logic-programming system [4], but I don't know how usable it is. [1] http://potassco.sourceforge.net/ [2] http://arxiv.org/abs/1006.4948 [3] http://pcgbook.com/wp-content/uploads/chapter08.pdf [4] http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pd... |
|
|
In this understanding, high-level (ASP, CSP) contrasts with low-level (SAT and SMT) for the same problem domain: just as with high- and low-level programming languages like Java are compiled down to low-level programming languages like x86 machine code, high-level formalism like ASP, CSP, ... can be compiled down to low-level SAT/SMT.
SAT/SMT is the assembly language of combinatorial problems because you have to state explicitly all forbidden solutions using CNF (conjuncive normal form). For examle if you have variables x, y and z, then the CNF ( x \/ y \/ not z ) /\ ( not x /\ not y ) has as models all maps from {x, y, z} to {0, 1} except {x=0, y=0, z=1}, {x=1, y=1, z=1} and {x=1, y=1, z=0}. The problem with using CNFs to enumerate forbidden solutions is that the formulae can be long (just like assembler programs can be long). With high-level formalisms like ASP you often get a much more succinct specification.
With a bit of squinting, you can even see first-order logic as a high-level formalism that compiles down to propositional logic (via skolemisation, resolution, unification, herbrand etc).