A Pearl on SAT and SMT Solving in Prolog
100 Current Papers in Artificial Intelligence, Automated Reasoning and Agent Programming. Number 2
Jacob M. Howe and Andy King, A Pearl on SAT and SMT Solving in Prolog, Theoretical Computer Science Volume 435, 1 June 2012, Pages 43-55.
DOI: http://dx.doi.org/10.1016/j.bbr.2011.03.031
Open Access: Available from Kent School of Computing Publication Index: http://www.cs.kent.ac.uk/pubs/2012/3136/index.html
I'm not sure quite how the terminology of a programming pearl arose. It denotes a neat, elegant or otherwise illuminating solution to some programming problem. In this case the programming pearl shows how a solver for a certain sort of logic can be programmed up in only 22 lines of of the Prolog Programming language.
Background (SAT): SAT stands for boolean satisfiability. Consider the two statements "either P is true and Q is false or R is true" and "either R is true and P is false or Q is true". There are a number of ways of making both these statements true. For instance if P, Q and R are all true then the two statements are true, similarly if R is true, and P and Q are both false then the statements are both true.
Statements consisting of letters representing facts that can be true or false, joined together with ands and ors form a logic called Propositional Logic. The letters are referred to as propositional variables (or just variables); the process of deciding whether they are true or false is referred to as assigning a truth value; and an assignment that makes all the statements true is said to satisfy them.
SAT solving is the process of taking statements in propositional logic and satisfying them. SAT solving is a major area of automated reasoning. The benchmark technique for SAT solving is called Davis-Putnam-Logemann-Loveland (just to make sure no one feels left out) and is frequently shorted to DPLL.
Background (Prolog): Prolog is a programming language which seeks to capture a more expressive form of logic (first order predicate logic) directly as a programming language. A statement in first order predicate logic looks something like: "For all x and y. If the only suspects in a murder are x and y and you know x didn't do it then y did it" - this is generally dressed up with mathematical symbols so it looks like ∀ x, y (only_suspects(x, y) & didnt_do_it(x)) → did_it(y). In Prolog this statement looks like
did_it(Y) :-
only_suspects(X, Y),
didn't_do_it(X).
When programming in Prolog I actually often end up thinking of it as a list of things to do in some particular order: e.g. "to find out who did it I need to find out who the suspects are and then find out which ones didn't do it". Prolog comes with built-in mechanisms for searching through possible assignments of names (like "the butler") to the variables (X, Y, etc.) which makes it an attractive language to use if you have a problem that is going to involve a lot of search. Prolog is a very clever language but it isn't a magic bullet for solving logic problems, a lot depends on the programmer's ability to express the problem in a way that Prolog can solve.
The agent programming languages I work with often look a lot like Prolog and, in particular, allow the agents to use Prolog to reason about their beliefs about the world. While I didn't necessarily want my agents to be SAT solving, 22 lines of code isn't a big overhead to make SAT solving available to them.
The SAT Solver: The SAT Solver in this paper uses the DPLL algorithm. A key part of that algorithm involves noticing that if you have a big disjunction (e.g. A or B or C or D or E or F) then you don't need to worry about what you need to do to make it true or false unless only one of the variables is left needing an assignment. In the Prolog solver this is done using something called a block declaration. This specifies that some part of the program isn't executed until certain conditions are met (like only one variable is left needing an assignment). The algorithm works by setting and blocking a watch on each of the big disjunctions in the problem which waits to see if it needs to assign a truth value to some variable in order to make that disjunction true - then the algorithm just merrily assigns true to each variable in turn until a watch statement fires and forces some particular assignment. If two watch statements fire and the assignments conflict then the search takes over and starts trying to assign false to some of the variables instead.
Sadly block declarations, while a pretty standard part of the Prolog language, aren't really one of its core features. My agents can't use block declarations so, sadly, I don't get a cute SAT solver for free out of this paper.
SMT Solving (briefly): Once you have a SAT solver you can use it to help you solve more complicated problems - for instance if you have a statement "either x < y or y > z and x + z = w" then you can replace "x < y" by P, "y > z" by Q and "x + z = w" by R and use a SAT solver to find an assignment for P, Q and R. From there you can use an algorithm for arithmetic (or similar) to see if that assignment will work for your problem, if it doesn't you go back and ask the SAT solver for a different assignment. This is called SMT solving (Satisfiability Modulo Theories). The paper goes on to code up an SMT solver in about 30 lines of Prolog.
The SAT and SMT solvers presented in the paper don't have performance that matches state-of-the-art solvers for these problems. However SAT and SMT solver development is driven by high profile competitions and case studies and state-of-the-art performance requires a lot of optimisation and that generally means complex and unintuitive code. However what the paper demonstrates is that respectable versions of these solvers can be created in a very clear fashion, at least in Prolog. In a problem domain where you need a little bit of SAT or SMT solving, but don't need a state of the art version that can cope with thousands of variables, then there may be good reasons (clear and understandable code, for instance) for using these versions.
This entry was originally posted at http://purplecat.dreamwidth.org/67842.html.
Jacob M. Howe and Andy King, A Pearl on SAT and SMT Solving in Prolog, Theoretical Computer Science Volume 435, 1 June 2012, Pages 43-55.
DOI: http://dx.doi.org/10.1016/j.bbr.2011.03.031
Open Access: Available from Kent School of Computing Publication Index: http://www.cs.kent.ac.uk/pubs/2012/3136/index.html
I'm not sure quite how the terminology of a programming pearl arose. It denotes a neat, elegant or otherwise illuminating solution to some programming problem. In this case the programming pearl shows how a solver for a certain sort of logic can be programmed up in only 22 lines of of the Prolog Programming language.
Background (SAT): SAT stands for boolean satisfiability. Consider the two statements "either P is true and Q is false or R is true" and "either R is true and P is false or Q is true". There are a number of ways of making both these statements true. For instance if P, Q and R are all true then the two statements are true, similarly if R is true, and P and Q are both false then the statements are both true.
Statements consisting of letters representing facts that can be true or false, joined together with ands and ors form a logic called Propositional Logic. The letters are referred to as propositional variables (or just variables); the process of deciding whether they are true or false is referred to as assigning a truth value; and an assignment that makes all the statements true is said to satisfy them.
SAT solving is the process of taking statements in propositional logic and satisfying them. SAT solving is a major area of automated reasoning. The benchmark technique for SAT solving is called Davis-Putnam-Logemann-Loveland (just to make sure no one feels left out) and is frequently shorted to DPLL.
Background (Prolog): Prolog is a programming language which seeks to capture a more expressive form of logic (first order predicate logic) directly as a programming language. A statement in first order predicate logic looks something like: "For all x and y. If the only suspects in a murder are x and y and you know x didn't do it then y did it" - this is generally dressed up with mathematical symbols so it looks like ∀ x, y (only_suspects(x, y) & didnt_do_it(x)) → did_it(y). In Prolog this statement looks like
did_it(Y) :-
only_suspects(X, Y),
didn't_do_it(X).
When programming in Prolog I actually often end up thinking of it as a list of things to do in some particular order: e.g. "to find out who did it I need to find out who the suspects are and then find out which ones didn't do it". Prolog comes with built-in mechanisms for searching through possible assignments of names (like "the butler") to the variables (X, Y, etc.) which makes it an attractive language to use if you have a problem that is going to involve a lot of search. Prolog is a very clever language but it isn't a magic bullet for solving logic problems, a lot depends on the programmer's ability to express the problem in a way that Prolog can solve.
The agent programming languages I work with often look a lot like Prolog and, in particular, allow the agents to use Prolog to reason about their beliefs about the world. While I didn't necessarily want my agents to be SAT solving, 22 lines of code isn't a big overhead to make SAT solving available to them.
The SAT Solver: The SAT Solver in this paper uses the DPLL algorithm. A key part of that algorithm involves noticing that if you have a big disjunction (e.g. A or B or C or D or E or F) then you don't need to worry about what you need to do to make it true or false unless only one of the variables is left needing an assignment. In the Prolog solver this is done using something called a block declaration. This specifies that some part of the program isn't executed until certain conditions are met (like only one variable is left needing an assignment). The algorithm works by setting and blocking a watch on each of the big disjunctions in the problem which waits to see if it needs to assign a truth value to some variable in order to make that disjunction true - then the algorithm just merrily assigns true to each variable in turn until a watch statement fires and forces some particular assignment. If two watch statements fire and the assignments conflict then the search takes over and starts trying to assign false to some of the variables instead.
Sadly block declarations, while a pretty standard part of the Prolog language, aren't really one of its core features. My agents can't use block declarations so, sadly, I don't get a cute SAT solver for free out of this paper.
SMT Solving (briefly): Once you have a SAT solver you can use it to help you solve more complicated problems - for instance if you have a statement "either x < y or y > z and x + z = w" then you can replace "x < y" by P, "y > z" by Q and "x + z = w" by R and use a SAT solver to find an assignment for P, Q and R. From there you can use an algorithm for arithmetic (or similar) to see if that assignment will work for your problem, if it doesn't you go back and ask the SAT solver for a different assignment. This is called SMT solving (Satisfiability Modulo Theories). The paper goes on to code up an SMT solver in about 30 lines of Prolog.
The SAT and SMT solvers presented in the paper don't have performance that matches state-of-the-art solvers for these problems. However SAT and SMT solver development is driven by high profile competitions and case studies and state-of-the-art performance requires a lot of optimisation and that generally means complex and unintuitive code. However what the paper demonstrates is that respectable versions of these solvers can be created in a very clear fashion, at least in Prolog. In a problem domain where you need a little bit of SAT or SMT solving, but don't need a state of the art version that can cope with thousands of variables, then there may be good reasons (clear and understandable code, for instance) for using these versions.
This entry was originally posted at http://purplecat.dreamwidth.org/67842.html.