Recursion and Induction Program Development Variable Ordering Greg Plaxton Theory in Programming Practice Spring 2005 Department of Computer Science University of Texas at Austin Program Development Today we will develop a Haskell program for the satisfiability problem As discussed in the previous lecture we will assume that the input is a CNF formula Such a formula is a conjunction of clauses Each clause is a disjunction of literals Each literal is either a variable or the negation of a variable Our implementation will use the Davis Putnam procedure outlined last time Theory in Programming Practice Plaxton Spring 2005 Representation of a Formula Each variable will be represented by an arbitrary string Each literal will be represented by a string consisting of a or symbol followed by the associated variable name The prefix indicates a variable that is not negated The prefix indicates a negated variable A clause will be represented as a list of literals A formula will be represented as a list of clauses Theory in Programming Practice Plaxton Spring 2005 Example of a Formula Consider the formula f equal to p q r p r q r p q r p q r We represent the formula f as follows p p q p p q r r r q r q r Theory in Programming Practice Plaxton Spring 2005 Types In our previous examples we have allowed Haskell to deduce the types In this example we will show how to define the types explicitly We use the following type definitions type Literal String type Clause Literal type Formula Clause Theory in Programming Practice Plaxton Spring 2005 Top Down Design Let us define a function that accepts a formula as input and returns a boolean indicating whether the formula is satisfiable If the formula is empty then the result is True If it contains an empty clause then the result is False Otherwise we choose some literal of the formula decompose the formula into two subformulae based on this literal solve each subformula recursively for satisfiability and return True if either returns True Theory in Programming Practice Plaxton Spring 2005 The Top Level Function dp We define our top level function dp as follows dp dp Formula xss xss emptyin xss otherwise Bool True False dp yss dp zss where v literal xss yss reduce v xss zss reduce neg v xss We have introduced a number of auxiliary functions that are discussed in greater detail on the next slide Theory in Programming Practice Plaxton Spring 2005 Functions used in dp emptyin xss returns True if xss has an empty clause literal xss returns a literal from xss where xss is nonempty and does not contain an empty clause neg v returns the string corresponding to the negation of v reduce v xss where v is a literal returns the formula obtained from xss by dropping any clause containing the literal v and dropping any occurrence of the literal neg v in each remaining clause Theory in Programming Practice Plaxton Spring 2005 The emptyin Function The code for emptyin is straightforward Does emptyin emptyin emptyin emptyin the formula contain an empty list Formula Bool False xss True xs xss emptyin xss Theory in Programming Practice Plaxton Spring 2005 The literal Function Function literal can return any literal from the formula It is easy to return the first literal of the first clause of its argument Since the formula is not empty and has no empty clause this procedure is valid Returns a literal from a formula It returns the first literal of the first list The list is not empty and it does not contain an empty list literal Formula Literal literal x xs xss x Theory in Programming Practice Plaxton Spring 2005 The neg Function The neg function is easy to code negate a literal neg Literal Literal neg var var neg var var Theory in Programming Practice Plaxton Spring 2005 The reduce Function A call to reduce v xss scans through the clauses of xss If xss is empty the result is the empty formula Otherwise for each clause xs If v appears in xs drop the clause If the negation of v appears in xs then modify xs by removing the negation of v If neither of the above conditions hold retain the clause Theory in Programming Practice Plaxton Spring 2005 The reduce Function Here is the code for the reduce function reduce a literal through a formula reduce Literal Formula Formula reduce v reduce v xs xss inl v xs reduce v xss inl neg v xs remove neg v xs reduce v xss otherwise xs reduce v xss Theory in Programming Practice Plaxton Spring 2005 Functions used in reduce Function reduce introduces two new functions which will be developed next inl v xs where v is a literal and xs is a clause returns True iff v appears in xs remove u xs where u is a literal known to be in clause xs return the clause obtained by removing u from xs Theory in Programming Practice Plaxton Spring 2005 The inl Function Here is the code for the inl function check if a literal is in a clause inl Literal Clause Bool inl v False inl v x xs v x inl v xs Theory in Programming Practice Plaxton Spring 2005 The remove Function Here is the code for the remove function remove a literal u from clause xs u is in xs remove Literal Clause Clause remove u x xs x u xs otherwise x remove u xs Theory in Programming Practice Plaxton Spring 2005 Refining our Implementation Currently we scan a clause to find a given literal Suppose we impose an order on the variables literals Then we could search more efficiently Furthermore we get to choose which variable to eliminate Use the order imposed above to determine the order of elimination When we eliminate a particular variable it is guaranteed to be associated with the first literal of any clause in which it appears Theory in Programming Practice Plaxton Spring 2005 The dp2 Function Function dp2 given below does the job of dp but it needs an extra argument like p q r which defines the variable ordering dp2 vlist xss xss True emptyin xss False otherwise dp2 wlist where v wlist yss zss yss dp2 wlist zss vlist reduce2 v xss reduce2 v xss We no longer need the functions inl remove and literal Theory in Programming Practice Plaxton Spring 2005 The reduce2 Function Here is the code for the reduce2 function reduce a literal through a formula reduce2 Literal Formula Formula reduce2 w reduce2 w x xs xss w x reduce2 w xss neg w x xs reduce2 w xss otherwise x xs reduce2 w xss Theory in Programming Practice Plaxton Spring 2005 A Further Improvement Note that reduce2 scans its argument list twice once for w and again for neg w We define reduce3 to scan the given list only once checking for both w and