3 ms·

Whenever I read about SAT solvers I think of Prolog and Minikanren and friends. Is there a relationship there? Do they use similar algorithms? I know that backt

Whenever I read about SAT solvers I think of Prolog and Minikanren and friends. Is there a relationship there? Do they use similar algorithms? I know that backtracking (mentioned in the article) is a thing in Prolog at least.

triska 7y ago
Yes, there are strong connections: In Prolog terminology, SAT is called CLP(B), constraint logic programming over Boolean variables, and several Prolog systems provide dedicated libraries to solve SAT instances efficiently. For instance, SICStus Prolog ships with a nice CLP(B) solver: https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.html/CLPB.html https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.ht... This particular solver uses Binary Decision Diagrams (BDDs) to model and solve SAT instances. CLP(B) blends in seamlessly with Prolog in the sense that Prolog variables and predicates are used to ask questions and obtain answers about satisfiability. For instance, we can formulate a Prolog query that asks: “Are there any X and Y such that the (X∧Y)∨X is satisfiable?” ?- sat(X*Y + X). X = 1, sat(Y=:=Y). The answer tells us that yes, the expression is satisfiable, if and only if X = 1. Moreover, we see from the answer that the truth value of the expression is then independent of Y, because Y is only constrained to be a Boolean variable (by the tautology Y⇔Y) and not involved in any other constraints. To obtain concrete assignments that make the expression true, we can use the library predicate labeling/1. On backtracking, all solutions are enumerated: ?- sat(X*Y + X), labeling([X,Y]). X = 1, Y = 0 ; X = Y, Y = 1. There are many different ways and approaches to implement SAT solvers, and this diversity is also reflected in Prolog implementations that provide them. For instance, in GNU Prolog, SAT solving is provided as a special case of integer constraints: http://www.gprolog.org/manual/html_node/gprolog061.html http://www.gprolog.org/manual/html_node/gprolog061.html The SAT solver of B-Prolog is so strong that it can compete with some dedicated SAT solvers. For a nice overview: https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-prolog/ https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-pr... A very nice SAT solver implementation in Prolog is explained in the paper A Pearl on SAT Solving in Prolog by Jacob M. Howe and Andy King: http://www.staff.city.ac.uk/~jacob/solver/flops.pdf http://www.staff.city.ac.uk/~jacob/solver/flops.pdf The paper shows that 20 lines of Prolog code suffice to implement an elegant solver for—as the authors put it—"solving some interesting, albeit modest, SAT instances". However, SAT is a quite low-level way to encode combinatorial tasks, and for this reason, CLP(FD/ℤ), i.e., constraint logic programming over finite domains/integers is typically used instead of SAT when solving combinatorial tasks with Prolog. Conceptually, we can think of CLP(ℤ) as a generalization of SAT solving, where variables can range over the entire integers instead of only 0 and 1. Strong and fast constraint solvers over integers are a major attraction of commercial Prolog systems, and often the key reason for buying one. From a logical perspective, propositional logic can be regarded as a special case of first-order predicate logic, so a language rooted in predicate logic, like Prolog, is also related to SAT solving in this way.

triska 7y ago

Yes, there are strong connections: In Prolog terminology, SAT is called CLP(B), constraint logic programming over Boolean variables, and several Prolog systems provide dedicated libraries to solve SAT instances efficiently. For instance, SICStus Prolog ships with a nice CLP(B) solver: https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.html/CLPB.html https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.ht... This particular solver uses Binary Decision Diagrams (BDDs) to model and solve SAT instances. CLP(B) blends in seamlessly with Prolog in the sense that Prolog variables and predicates are used to ask questions and obtain answers about satisfiability. For instance, we can formulate a Prolog query that asks: “Are there any X and Y such that the (X∧Y)∨X is satisfiable?” ?- sat(X*Y + X). X = 1, sat(Y=:=Y). The answer tells us that yes, the expression is satisfiable, if and only if X = 1. Moreover, we see from the answer that the truth value of the expression is then independent of Y, because Y is only constrained to be a Boolean variable (by the tautology Y⇔Y) and not involved in any other constraints. To obtain concrete assignments that make the expression true, we can use the library predicate labeling/1. On backtracking, all solutions are enumerated: ?- sat(X*Y + X), labeling([X,Y]). X = 1, Y = 0 ; X = Y, Y = 1. There are many different ways and approaches to implement SAT solvers, and this diversity is also reflected in Prolog implementations that provide them. For instance, in GNU Prolog, SAT solving is provided as a special case of integer constraints: http://www.gprolog.org/manual/html_node/gprolog061.html http://www.gprolog.org/manual/html_node/gprolog061.html The SAT solver of B-Prolog is so strong that it can compete with some dedicated SAT solvers. For a nice overview: https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-prolog/ https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-pr... A very nice SAT solver implementation in Prolog is explained in the paper A Pearl on SAT Solving in Prolog by Jacob M. Howe and Andy King: http://www.staff.city.ac.uk/~jacob/solver/flops.pdf http://www.staff.city.ac.uk/~jacob/solver/flops.pdf The paper shows that 20 lines of Prolog code suffice to implement an elegant solver for—as the authors put it—"solving some interesting, albeit modest, SAT instances". However, SAT is a quite low-level way to encode combinatorial tasks, and for this reason, CLP(FD/ℤ), i.e., constraint logic programming over finite domains/integers is typically used instead of SAT when solving combinatorial tasks with Prolog. Conceptually, we can think of CLP(ℤ) as a generalization of SAT solving, where variables can range over the entire integers instead of only 0 and 1. Strong and fast constraint solvers over integers are a major attraction of commercial Prolog systems, and often the key reason for buying one. From a logical perspective, propositional logic can be regarded as a special case of first-order predicate logic, so a language rooted in predicate logic, like Prolog, is also related to SAT solving in this way.