SAT solver of Howe & King as a logic program
Howe and King [HK11b,HK11a] presented a SAT solver which is an elegant and concise Prolog program of 22 lines. It is not a logic program, as it includes some extra-logical features of Prolog; it was constructed as an implementation of the DPLL algorithm, using logical variables and coroutining. Here we construct this program using the Logic + Control principle of Kowalski. We show how the program can be constructed by adding control to an initial logic program. We discuss correctness, completeness, termination and non-floundering of the program. In particular, we outline a formal proof of correctness and completeness of the underlying logic program. The presented proof methods may be of separate interest.
Sections 1 and 2 present an introductory SAT solver, which is a simple logic program. Section 3 presents methods of proving correctness and completeness of logic programs, and applies them to the program from the previous section. Section 4 presents the actual construction of the program of [HK11b]. To facilitate the intended control flow, the program from Section 2 is first converted into a more sophisticated logic program. Then the control is added by modifying the Prolog selection rule and pruning some redundant fragments of the search space. Properties of the constructed program are discussed in Section 5. Section 3 and the fragments of Section 5 concerning correctness and completeness may be skipped at the first reading.
Here we describe how formulae in CNF are represented in the program of [HK11b]. Propositional variables are represented as logical variables. A literal of a clause is represented as a pair of a variable and of true or false; a positive literal, say x, as true-X and a negative one, say ¬x, as false-X. A clause is represented as a list of (representations of) literals, and a conjunction of clauses as a list of their representations. For instance a formula (x ∨¬y ∨ z) ∧ (¬x ∨ v) is represented as [[true-X,false-Y,true-Z],[false-X,true-V]]. Thus a clause is satisfiable iff its representation has an instance containing a pair of the form t-t, i.e. false-false or true-true. A formula in CNF is satisfiable iff its representation has an instance whose each element (is a list which) contains a t-t.
To avoid confusion, the clauses of programs will be called rules. We will use the grey color to mark intermediary versions of rules, not included in the final program, while the rules of the final program are typeset in blue.
We first construct a logic program P1 checking satisfiability of CNF formulae represented as above. We will say “formula f” for a formula in CNF represented as a term f. We use the predicate names from [HK11b] (which may be not adequate for our declarative view of the program).
L1 be the set of those lists of ground terms that contain an element of the form t-t,
L2 be the set of lists, whose all elements are from L1.
We construct a program defining L2. Following [HK11b], the predicate defining this set will be called problem_setup. Thus, for a formula f, a query problem_setup(f) will fail for an unsatisfiable f and succeed when f is satisfiable. In this way the predicate checks the satisfiability of f. Moreover, the computed answer substitutions provide bindings of truth values to variables of f, under which f is true.
To represent the binding as a list of truth values, we introduce the main predicate sat∕2 of the program. It defines the relation in which the first argument is from L2 and the second argument is a list of truth values (i.e. of true or false).1 The intended query is sat(f,l) where l is the list of variables of a formula f. Such query succeeds iff f is satisfiable. At success l is instantiated to a list of truth values representing a valuation satisfying f. Predicate sat is defined by an obvious rule:
sat(Clauses, Vars) :- problem_setup(Clauses), elim_var(Vars).
where elim_var defines the set of lists of truth values. We follow [HK11b]:
elim_var([ ]). elim_var([Var | Vars]) :- elim_var(Vars), assign(Var). assign(true). assign(false).
It remains to construct a definition of predicate problem_setup. We do this in a rather obvious way, using a predicate clause_setup, which defines the set L1.
problem_setup([ ]): problem_setup([Clause|Clauses]) :- clause_setup(Clause), problem_setup(Clauses). clause_setup([Pol-Var|Pairs]) :- Pol = Var. clause_setup([Pol-Var|Pairs]) :- clause_setup(Pairs).
This completes the construction of the logic program P1.2
It may be obvious for the reader that the constructed program indeed defines the required relations. However we discuss now how to formally prove this fact. The reader may prefer to skip this section at the first reading, and proceed to Section 4. We employ the approach of [DM05, Chapters 3.1 and 3.3]. We present simpler (and less general) versions of the correctness and completeness criteria from [DM05]. We consider definite clause programs; for programs with negation see [DM05].
We provided a specification for the program P1: for each its predicate a corresponding relation has been given; the predicate should define this relation. Below we introduce some notions which depend on the considered specification. We will however often skip a phrase “with respect to specification …”, as our specification is fixed for this section.
Let us call a ground atom p(t1,…,tn) specified if the tuple (t1,…,tn) is in the relation corresponding to p. So in our case, the specified atoms are of the form sat(t,u), elim_var(u), problem_setup(t), clause_setup(s), x= x, assign(true), assign(false), where s L1, t L2, u is a list whose elements are true or false, and x is an arbitrary ground term. Let S denote the set of specified atoms. S can be seen as a Herbrand interpretation representing the specification.
In imperative programming, correctness usually means that the program results are as specified. In logic programming, due to its non-deterministic nature, we have actually two issues: correctness (all the results are compatible with the specification) and completeness (all the results required by the specification are produced). In other words, correctness means that the relation defined by the program is a subset of the specified one, and completeness means inclusion in the opposite direction. In terms of specified atoms and the least Herbrand model MP of a program P we have: P is correct iff MP ⊆ S; it is complete iff MP ⊇ S.
for each ground instance H ← B1,…,Bn of a rule of the program, if B1,…,Bn are specified atoms then H is a specified atom.
The reader is encouraged to check that P1 satisfies this condition.3 Thus P1 is correct.
Our criterion for proving completeness is less general. It will show that for a given query (or a class of queries) the program will produce all the answers required by the specification. Let us say that a program P is complete for an atomic query A if, for any specified ground instance Aθ of A, Aθ is in MP . Generally, the program is complete for a query Q = A1,…,An if, for any ground instance Qθ of Q where A1θ,…,Anθ are specified atoms, A1θ,…,Anθ MP .
A ground atom H is called covered [Sha83] if it is the head of a ground instance H ← B1,…,Bn of a rule of the program, such that all the atoms B1,…,Bn are specified.
Let us apply this criterion to our program. Consider a query Q=sat(t,l) where t,l are (possibly non-ground) lists of a fixed length (i.e. terms of the form [t1,…,tn]), and each element of t is a list of a fixed length. The intended queries to the program are of this form. For such queries the program terminates, under any selection rule.5 Thus there exists a finite SLD-tree for each such query. The reader is encouraged to check that each specified atom is covered.6 Hence the program is complete for the intended initial queries, and it terminates for such queries.7
As a final comment, we point out that our specification describes exactly the least Herbrand model MP1 of the program. This is often not the case, MP is specified approximately, by giving separate specifications Scompl,Scorr for completeness and correctness; it is required that Scompl ⊆ MP ⊆ Scorr. The specifications describe, respectively, which atoms have to be computed, and which are allowed to be computed. A standard example is the usual definition of append, where it is difficult (and unnecessary) to specify the exact defined relation [DM05].8
In this section we modify the program P1 to improve its efficiency. To be able to influence its control in the intended way, we first construct a more sophisticated logic program P2. We modify the definition of clause_setup∕1, introducing some new predicates.
Program P1 performs inefficient search by means of backtracking. We improve it by delaying unification of pairs Pol-Var in clause_setup. The idea is to perform such unification if Var is the only unbound variable of the clause.9 Otherwise, clause_setup is to be delayed until one of the first two variables of the clause is bound to true or false. The actual binding may be performed by other invocation of clause_setup, or by elim_var.
This idea will be implemented by separating two cases; the clause has one literal, or it has more literals. For efficiency reasons we want to distinguish these two cases by means of indexing the main symbol of the first argument. So the argument should be the tail of the list. (The main symbol is [ ] for a one element list, and [ | ] for longer lists.) We redefine clause_setup, introducing an auxiliary predicate set_watch∕3. It defines the same set L1 as clause_setup does, but a clause [Pol-Var|Pairs] is represented as three arguments Pairs,Var,Pol of set_watch.
clause_setup([Pol-Var | Pairs]) :- set_watch(Pairs, Var, Pol). set_watch(, Var, Pol) :- Var=Pol. set_watch([Pol2-Var2 | Pairs], Var1, Pol1) :- watch(Var1, Pol1, Var2, Pol2, Pairs).
The first rule of set_watch expresses the fact that a clause [Pol-Var] is in L1 iff Pol=Var; the clause is represented as three arguments [ ],Var,Pol of set_watch. We now explain the second rule.
In set_watch, delaying is to be controlled by the variables of the first two literals of the clause; so the variables should be separate arguments of a predicate. Thus we introduce an auxiliary predicate watch∕5. It defines the set of lists from L1 of the length > 1; however a list [Pol1-Var1,Pol2-Var2 |Pairs] is represented as the five arguments Var1,Pol1,Var2,Pol2,Pairs of watch. Executing watch(Var1,Pol1,Var2,Pol2,Pairs) is to be delayed until Var1 or Var2 is bound. This is achieved by a declaration
:- block_watch(-, ?, -, ?, ?).
watch(Var1, Pol1, Var2, Pol2, Pairs) :- Var1=Pol1: watch(Var1, Pol1, Var2, Pol2, Pairs) :- set_watch(Pairs, Var2, Pol2).
However the first rule may bind Var1, which we want to avoid. We know that watch will be selected with its first or third argument bound. Thus we introduce an auxiliary predicate update_watch∕5. Declaratively, it defines Sthe same relation as watch, it can be defined by the two rules above (with watch replaced by update_watch). The intention is to call it with the first argument bound. Predicate watch can be defined by a rule with the head
watch(Var1, Pol1, Var2, Pol2, Pairs)
and the body
update_watch(Var1, Pol1, Var2, Pol2, Pairs)
update_watch(Var2, Pol2, Var1, Pol1, Pairs).
Both define the required relation. We want to choose the body dynamically, to assure that update_watch is called with its first argument bound. In other words, the logic program P2 contains two rules for watch; the control has to choose one of them and abandon the other. We do not see a way of doing this by adding control to a logic program. So we use extra-logical features of Prolog.
watch(Var1,Pol1, Var2, Pol2, Pairs) :- nonvar(Var1) -> update_watch(Var1, Pol1, Var2, Pol2, Pairs) ; update_watch(Var2, Pol2, Var1, Pol1, Pairs).
Notice that the program containing such rule is not a logic program, due to the built-in nonvar and the if-then-else construct.
Our logic program contains the following rules defining update_watch.
update_watch(Var1, Pol1, Var2, Pol2, Pairs) :- Var1=Pol1. update_watch(Var1, Pol1, Var2, Pol2, Pairs) :- set_watch(Pairs, Var2, Pol2).
If the first argument of the initial query sat(f,l) is a (representation of a) propositional formula then update_watch is called with its second argument true or false. As the first argument is bound, the unification Var1 = Pol1 (in the first rule above) does not bind any variable. Thus if the first rule succeeds then no variables are bound and there is no point in invoking the second rule;10 the search space should be pruned accordingly. We do this by converting the two rules into
update_watch(Var1, Pol1, Var2, Pol2, Pairs) :- Var1=Pol1 -> true; set_watch(Pairs, Var2, Pol2).
The unification Var1 = Pol1 can be replaced by == of Prolog, because – as explained above – it works here only as a test. The program in [HK11b] uses ==.
This completes the construction of the Prolog program from [HK11b]. The program consists of the rules for predicates sat, elim_vars, assign, problem_setup, clause_setup, set_watch, watch, update_watch, written with a normal size font. It differs from its declarative version P2 by the rules for watch and update_watch. The control has been added to P2 by (1) changing the default Prolog selection rule (by the block declaration), and (2) pruning some redundant parts of the search space (by the if-then-else constructs in the rules for watch and update_watch).
The final Prolog program can be seen as the logic program P2 with a specific control. The default selection rule of Prolog is modified by a block declaration. The search space is pruned by removing some redundant parts of SLD-trees. The pruning could be done by employing the cut; here a more elegant solution was used, with the if-then-else construct of Prolog.
P2 differs from the logic program P1 by the fragment related to predicate clause_setup, defining the set L1. We divided the set of lists L1 into the the subset L1,1 of those of length 1, and L1,2 of those of length > 1; the two sets are defined separately. To facilitate the intended control flow we introduced a few predicates defining the same set L1,2, however they use different representation of the elements of L1,2.
We gave a specification for both programs, providing for each predicate the relation it defines. So the specified atoms are those of the form sat(t,u), elim_var(u), assign(true), assign(false), problem_setup(t), clause_setup(s), set_watch(s0,v,p), watch(v1,p1,v2,p2,s0), update_watch(v1,p1,v2,p2,s0), x = x, where t L2, u is a list of truth values, s L1, [p-v|s0] L1, [p1-v1,p2-v2|s0] L1, and x is an arbitrary ground term. Program P2 is correct with respect to the specification; this can be proved by applying the correctness criterion from Section 3. The reader is encouraged to construct the proof.
We do not include here the details of the correctness and completeness proofs for P1 and P2, as they are simple and rather obvious (conf. Footnote 3 presenting one of more sophisticated cases). Let us remark that an error in one of the rules in an earlier draft has been found while constructing a correctness proof, as the correctness criterion was violated. This illustrates practicality of the proof methods.
The reader is also encouraged to prove that all the specified atoms are covered by P2. Hence P2 is complete for any terminating query, by the sufficient condition from Section 3. The completeness is not violated when one (the first or the second) rule for watch is removed from P2 (as all the specified atoms are covered by P2 without the clause).
Program P2 terminates for any intended query. This can be justified in a similar way as termination of P1 (conf. Footnote 5). The termination holds for any selection rule, in particular for that of Prolog with (arbitrary) delay declarations.
The employed methods of proving correctness, completeness, and termination of logic programs are not applicable to the final Prolog program, as it contains the Prolog conditional and nonvar. We informally justified that the two procedures, which differ in P2 and in the Prolog program, will behave in the same way.11
It remains to show that the Prolog program does not flounder, i.e. that each delayed atom is eventually selected. (The same holds for P2 with the block declaration.) Assume that the initial query is sat(f,l) where f is a representation of a propositional formula, l is a fixed length list, and that each variable occurring in f occurs in l. Notice that the intended initial goals are of this form. In each non failed derivation, elim_var∕1 will eventually bind all the variables of l, and hence all the variables of f. Thus all the delayed atoms will be selected.
This paper presents an example of constructing a Prolog program using the Logic + Control approach of Kowalski, and shows that part of the related reasoning can be formalized in a rather simple and natural way. We constructed the SAT solver of Howe and King [HK11b, HK11a]. The initial simple logic program P1 was first transformed to another logic program P2, in order to facilitate modifying the control in the intended way. This step could be seen as adding new representation of data (the formula represented as a single argument of clause_setup is represented as a few arguments of the newly introduced predicates). Then control was added to P2, by fixing the selection rule and pruning the search space.
We discussed correctness, completeness, and termination of the three programs, and non-floundering of P2 and the final program. In particular, we outlined formal proofs of correctness and completeness of P1 and P2. The presented sufficient conditions for correctness and completeness of logic programs may be of separate interest. They can be seen as formalizing common-sense ways of reasoning about programs. The condition for correctness is known since 1979 but seems neglected. A stronger form of both conditions is discussed in [DM05]. The author believes that such proof methods, possibly treated informally, are a useful tool for practical reasoning about actual programs. The formal proofs outlined in this paper support this claim.
[Dra99] W. Drabent. It is declarative: On reasoning about logic programs. Technical report, 1999. http://www.ipipan.waw.pl/~drabent/itsdeclarative3.ps.gz. A poster abstract in Logic Programming: The 1999 International Conference, p. 607, The MIT Press.
[HK11b] J. M. Howe and A. King. A pearl on SAT solving in Prolog (extended abstract). Logic Programming Newsletter, 24(1), March 31 2011. http://www.cs.nmsu.edu/ALP/2011/03/a-pearl-on-sat-solving-in-prolog-extended-abstract/.
- Note that the arguments are not related, the relation is the Cartesian product of L2 and the set of truth value lists.
- Following the style of [HK11b], we used a Prolog built-in =, which defines the relation of term equality. Formally, it should be assumed that P1 contains also a unary rule =(X,X), defining the built-in.
- For instance consider the last rule of the program, and its arbitrary ground instance clause_setup([p-v|s]) ← clause_setup(s). If clause_setup(s) is specified then s L1, hence [p-v|s] L1 and clause_setup([p-v|s]) is specified.
- The notion of completeness used here is weaker than that of [DM05]. Also, this sufficient condition for completeness is, strictly speaking, not an instance of that given in [DM05]. Its correctness follows from [Dra99, Prop. 5.1.1].
- Informally: The predicates are invoked with fixed length lists as arguments, each recursive call employs a shorter list. Formally: The program is recurrent [Apt97] and the
query is bounded, under a suitable level mapping (based on the length of the lists from L1, and the sum of the lengths of the element lists for the lists from L2).
- For instance consider a specified atom A = problem_setup(t). Thus t is a ground list of elements from L1. If t is nonempty then t = [s|t′], where s L1, t′ L2. Thus a ground instance A ← clause_setup(s),problem_setup(t′) of a clause of P1 has all its body atoms specified, so A is covered. If t is empty then A is covered as it is the head of the rule problem_setup().
- Moreover, this reasoning applies to any query which is a specified atom. Hence the program is complete
- Notice that in our case we are not interested in any answers where the argument is a list, or a list of lists, with an element which is not a pair of truth values (for instance an answer like clause_setup([a,true-true])). So it may be considered natural to require completeness w.r.t. a specification which instead of L1 uses the set L1′ of those elements of L1 which are lists of pairs of truth values, and instead of L2 uses the set of those lists whose elements are from L1′.
- The clause which is (represented as) the argument of clause_setup in the rule for problem_setup.
- Because the success of the first rule produces the most general answer for update_watch(…), which subsumes any other answer.
- Notice that the informal justification for search space pruning in procedure update_watch is based on the assumption that the first argument of the initial query sat(f,l) is a representation of a propositional formula. So we do not know if the Prolog program is complete for initial queries with the first argument not of this form.