4The Benefits of Pattern-Match-Oriented Programming

The purpose of this chapter is to clarify in what situations and how pattern-match-oriented programming is useful. All the examples in the previous chapters involved only single matchAll or match expressions, but in this chapter we examine what role Egison's pattern matching plays in the writing of larger programs.

4.1Implementing a SAT Solver

To observe the benefits of pattern-match-oriented programming in the context of writing a reasonably large program, we implement a SAT solver. A SAT solver is a program that determines whether there exists an assignment of truth values to logical variables that makes a given propositional formula true. The logical formulas taken as input by SAT solvers are typically in conjunctive normal form. A logical formula is in conjunctive normal form when it is a conjunction of clauses, each of which is a disjunction of literals. A literal is a formula of the form \(p\) or \(\neg p\). For example, \((p \lor q) \wedge (\neg p \lor r) \wedge (\neg p \lor \neg r)\) is a formula in conjunctive normal form that becomes true under the assignment \(p = \texttt{False}\), \(q = \texttt{True}\), \(r = \texttt{True}\).

4.1.1The Davis-Putnam Algorithm

Here we implement the Davis-Putnam algorithm [3], a relatively simple algorithm among those for solving SAT problems. In the implementation of this section, propositional formulas in conjunctive normal form are represented as a collection of collections of literals. Since \(\wedge\) and \(\lor\) are commutative operators, this collection of collections can be pattern-matched as a multiset of multisets of literals. Furthermore, literals are represented as integers: a literal of the form \(p\) is a positive integer, and a literal of the form \(\neg p\) is the negation (multiplied by \(-1\)) of the positive integer corresponding to \(p\).

Then, the matcher for these formulas can be defined as multiset (multiset integer). The following program is the core implementation of the Davis-Putnam algorithm. The dp function takes a list of logical variables and a formula as arguments, and returns True if a solution exists and False otherwise. The type annotation indicates that the dp function takes a list of integers (logical variables) and a list of lists of integers (a formula) and returns a Bool.

def dp (vars: [Integer]) (cnf: [[Integer]]) : Bool :=
  match (vars, cnf) as (multiset integer, multiset (multiset integer)) with
  | (_, []) -> True
  | (_, [] :: _) -> False
  -- 1-literal rule
  | (_, ($l :: []) :: _) -> dp (delete (abs l) vars) (assignTrue l cnf)
  -- pure literal rule (positive)
  | ($v :: $vs, !((#(neg v) :: _) :: _)) -> dp vs (assignTrue v cnf)
  -- pure literal rule (negative)
  | ($v :: $vs, !((#v :: _) :: _)) -> dp vs (assignTrue (neg v) cnf)
  -- otherwise
  | ($v :: $vs, _) ->
    dp vs
       ((resolveOn v cnf) ++ (deleteClausesWith v (deleteClausesWith (neg v) cnf)))

The first match clause (line 3) states that if the input formula is empty, then it is satisfiable. The second match clause (line 4) states that if the input formula contains an empty clause, then no solution exists. The third match clause (line 6) represents the 1-literal rule. When the input formula has a clause consisting of a single literal, we can immediately assign True to that literal. The fourth match clause (line 8) states that if the negation of a certain logical variable does not appear as a literal at all, then we can immediately assign True to that variable. For example, \((p \lor q) \wedge (\neg p \lor r) \wedge (\neg p \lor \neg r)\) does not contain the negation of the logical variable \(q\), so True can be assigned to \(q\). The fifth match clause (line 10) expresses the converse of the fourth match clause. This clause states that if only the negation of a certain logical variable appears in the input formula, then False can be assigned to that variable. The last match clause (lines 12--14) applies the resolution principle. This clause enumerates all pairs of clauses of the form \(p \lor C\) and \(\neg p \lor D\) (where \(C\) and \(D\) are disjunctions of literals) and generates clauses of the form \(C \lor D\).

The above definition of dp describes all the rules for simplifying the input formula using pattern matching on multisets. In traditional functional programming, achieving the same thing would require combining multiple library functions or defining auxiliary functions. An OCaml implementation of the Davis-Putnam algorithm can be found in [3].

4.1.2The Resolution Principle

This section presents the implementation of the resolveOn function. We begin by presenting a naive implementation. The resolveOn function can be defined using a matchAll expression as follows. The type annotation indicates that the resolveOn function takes an integer v and a formula cnf and returns a list of derived clauses.

def resolveOn (v: Integer) (cnf: [[Integer]]) : [[Integer]] := matchAll cnf as multiset (multiset integer) with
| (#v :: $xs) :: (#(negate v) :: $ys) :: _ -> unique (filter (\c -> not (tautology c)) (xs ++ ys))

The pattern for enumerating pairs of clauses of the form \(p \lor C\) and \(\neg p \lor D\) can be described using pattern matching on a multiset of multisets. However, this alone would also match cases where \(C \lor D\) is a tautological clause (which happens when \(C\) contains a literal \(q\) and \(D\) contains a literal \(\neg q\)). To handle this, the filter function and the tautology function are used to remove such clauses. By defining the resolveOn function using sequential not patterns (Section 3.3 of Chapter 3), such operations can be incorporated into the pattern itself.

def resolveOn (v: Integer) (cnf: [[Integer]]) : [[Integer]] :=
  matchAll cnf as multiset (multiset integer) with
  | {(#v :: (@ & $xs)) :: (#(neg v) :: (@ & $ys)) :: _,
     !($l :: _, #(neg l) :: _)}
    ->  unique (xs ++ ys)

4.2Separating Two Kinds of Loops

The SAT solver implemented in Section 4.1 contained a loop that could not be eliminated by pattern-match-oriented programming. That loop is the recursion of the dp function. This recursion is an essential loop for narrowing the search space in solving SAT problems. This search space reduction cannot be achieved by a simple backtracking algorithm. In contrast, all other loops that can be implemented through backtracking have been pushed into the patterns. In traditional functional programming, both kinds of loops had to be written using recursion. Pattern-match-oriented programming confines loops implementable by backtracking into patterns, allowing programmers to focus solely on writing the essential loops that reduce time complexity. This improves both the ease of writing and the readability of programs.