contradict.lsp0000644000175000017500000004554110737055774013562 0ustar cremlaecremlae#
 Name: Omer Baror

 Please note the comment in section "Other Pruning Events" about the
 conversation I had with Sam Luckenbill that affected my program.
#
; (provecontradiction clauses): given clauses (a list of logical clauses
; in clause form) this function returns either a tree showing how it
; derived a contradiction (using resolution), or "FAIL," meaning that no
; contradiction could be found.
;
; Clause form, in this context, is a list of literals which is treated as
; a clause with the disjunction of each of those literals. A literal is
; either any symbol or the negation of any symbol, where negation is
; shown with a twoelement list, the first element of which is the word
; "not" and the second of which is the negated symbol.
;
; A derivation tree is a tree, the internal nodes of which are
; threeelement lists, and the leaf nodes of which are singleelement
; lists. The leaves are clauses from the input, and each internal node is
; of the form (c r1 r2) where c is the clause this node represents and r1
; and r2 are the clauses that resolve into c.
;
; This function works by first doing preprocessing on clauses,
; then calling proveaux, which derives a contradiction if one exists, and
; finally doing postprocessing to get the solution in the requested form.
; The preprocessing done is with functions buildds and addsort. buildds
; turns the clauses into a clause nodes for proveaux, and addsort sorts
; them by their fcost (see proveaux for a description of fcost).
; proveaux treats the clauses as a priority queue, running through each
; one, resolving it with the rest, and inserting the results back onto
; the queue. And, it stops when a contradiciton is found.
; The postprocessing done is to first reverse the solution from proveaux
; so that the contradicting node (with a nil clause) is first in the list,
; then checking if that node actually is nil (if not, we failed to find a
; contradiction). Then, it sorts this solution by the number of steps
; required to reach that step. It does this so that, when buildsol builds
; the solution, it never needs to backtrack (see buildsol).
(defun provecontradiction (clauses)
(cond ((null clauses) (list ())) ; just in case our list is empty...
(t (let ((pre_sol (reverse (proveaux (addsort (buildds clauses 0)) ; get proveaux's solution
(length clauses)))))
(cond ((not (null (third (car pre_sol)))) 'FAIL) ; if proveaux failed
((null pre_sol) 'FAIL) ; case in which buildds determined all clauses as vacuously true
(t (buildsol (cons (car pre_sol) ; build a solution
(reversecarsort (cdr pre_sol))) ; sort cdr of list for ease of building
(cadr (car pre_sol))))))))) ; root is first element in list
; (proveaux clauses n): given clauses (a list of clause nodes (see
; buildds)) with ids less than n, this function adds to clauses using
; resolution until it finds a contradiction. It uses n to number the nodes
; it adds. It returns a list of clause nodes including the contradiction
; and any other node that could possibly have led to that contradiction,
; with the contradiction itself always as the last element of the list. If
; no contradiction is found, it returns all clauses it found.
; The list of clauses is a priority queue, which prioritizes clauses that
; are more likely to be optimal solutions. The way it does this is similar
; to A* tree search: it adds the depth of the tree derivation to this node
; (g(x)) with the number of elements left to resolve in the clause (h(x)).
; Because only one element can be resolved at a time, h(x) is an admissible
; heuristic to predict solution depth from this node. Hence, organizing our
; list of clauses according to f(x)=g(x)+h(x) ensures that when we choose a
; node with h(x)=0 for expansion (a contradiction), it is the end of the
; optimal path to a contradiction.
; To ease postproduction (see provecontradiction), this function drops
; from its final solution any clause that is obviously not part of the
; solution, that is, any node whose fcost is greater than the gcost to
; our solution (because, obviously, we didn't use this node in any
; resolution).
(defun proveaux (clauses n)
(cond ((null clauses) nil) ; No more clauses to analyze... Return.
((null (third (car clauses))) ; Contradiction!
(append (dropbig (cdr clauses) (car (car clauses))) ; drop unnecessary nodes
(list (car clauses)))) ; make sure contradiction is last
(t (let ((addition (onestepresolve (car clauses) ; resolve car
(cdr clauses) ; with all of cdr
n)))
(cons (car clauses) ; This node was expanded, so it might be in the solution
(proveaux (removecaddrdups ; prune clauses by removing duplicates
(mergenodes (cdr clauses) ; merge current clause list
(addsort addition))) ; with the new clauses
(+ n (length addition)))))))) ; create new n
; (buildds clauses n): given a list of clauses in clause form (see
; provecontradiction) and a node id, this function returns the a list of
; clause nodes that matches the clauses, where each node is numbered
; incrementally, starting with n.
;
; The data structure has two forms, for leaf nodes and for internal nodes.
; Leaf nodes look like: (gcost id clause)
; Internal nodes look like: (gcost id clause rid1 rid2)
; Where...
; gcost: number of resolutions required to reach this node (see proveaux)
; id: this node's id (a unique number associated with the node)
; clause: the clause this node represents
; rid1: the id of one node used in the resolution to create this node.
; rid2: the id of the other node used to create this node.
;
; We use this data structure because it is concise enough to let us add
; many nodes to our list (see proveaux) before running out of space, but
; it retains all of the information we need to construct a solution out of
; a list of nodes (see buildsol), which means that we don't have to search
; the nodes in a depthfirst fashion to construct the path to the node.
;
; Note: all clauses passed to buildds are, by definition, leaf clauses,
; so each has a gcost of 0 and only three elements.
;
; Note 2: just in case we have bad input, we run hasnegate and removedups
; on all clauses before bothering to add them to our list.
(defun buildds (clauses n)
(cond ((null clauses) nil) ; no more clauses to build
((hasnegate (car clauses)) (buildds (cdr clauses) (+ n 1))) ; bad clause, only add the rest
(t (cons (list 0 n (removedups (car clauses))) ; build the node, removing duplicate literals
(buildds (cdr clauses) (+ n 1)))))) ; add the rest
; (buildsol clauses id): given a list of clause nodes, sorted in reverse
; order by gcost, and the id of some node in that list, this function
; returns a tree of the kind requested by the solution (see
; provecontradiction). It runs recursively by first finding the node,
; and if the node is a leaf, simply returning the clause of that node as
; the only node in a tree. If, on the other hand, the node is an internal
; node, the function returns a tree with the clause as a root, and the
; results of running recursively on each of the nodes used to build
; this one as its two children.
; Because the nodes are stored in reverse order by gcost, when running
; recursively, we are guaranteed that the parents are located later in the
; list than this node, because their cost has to be at most one less than
; than the cost to reach this node.
(defun buildsol (clauses id)
(cond ((not (= (cadr (car clauses)) id)) (buildsol (cdr clauses) id)) ; wrong node, keep going)
((= (length (car clauses)) 3) (list (third (car clauses)))) ; leaf node
(t (list (third (car clauses)) ; internal node, built tree with the clause
(buildsol (cdr clauses) (fourth (car clauses))) ; first child
(buildsol (cdr clauses) (fifth (car clauses))))))) ; second child
# ##### Resolution Functions ##### #
; (onestepresolve v l n): given a single node v, a list of other nodes l,
; and a minimum id n, this function returns the list of nodes that result
; from applying resolution between v and each element in l, where the
; resulting nodes are numbered incrementally from n.
; It works by using the litresolve function to compute a single
; resolution, and if that resolution succeeded, building a node for it.
(defun onestepresolve (v l n)
(cond ((null l) ()) ; no more nodes to resolve
(t (let ((res (litresolve (third v) ; resolve with v's clause...
(third (car l)) ; ... car l's clause...
(third v)))) ; ... and v's clause...
(cond ((null (car res)) (onestepresolve v (cdr l) n)) ; failed
(t (cons (list (+ 1 (max (car v) (car (car l)))) ; succeeded: build new node
n ; id
(removedups (cadr res)) ; remove duplicate literals from the clause
(cadr v) ; rid1
(cadr (car l))) ; rid2
(onestepresolve v (cdr l) (+ n 1))))))))) ; continue
; (litresolve a b orig_a): given two clauses b and orig_a, and clause a,
; which is a subset of orig_a, this function returns a twoelement list.
; The first element is either t or nil, depending on whether applying
; resolution was successful or not, and the second element is the result
; of the resolution, that is, every element in b and orig_a except for
; the resolved literal from each. It works by recursively running through
; the list a, comparing it to the first element in b, and when a runs out,
; running recursively on (orig_a (cdr b) orig_a), that is, resetting a and
; moving on to the next element in b. If it finds a match, it checks if
; there are any _more_ matches. If there are, then the resolution leads to
; a vacuous truth (because the resolution will have something like A or
; NOT A or ..., which is always true), and we can throw it out as useless
; (see hasnegate). If there are no more matches, it returns a list with
; all elements in b except for the match and all elements in orig_a except
; for the match. Note that because we iterate through b, if we run
; recursively on (cdr b), we have to readd (car b) to the solution, since
; it is a unique literal in b.
(defun litresolve (a b orig_a)
(cond ((null b) (list nil nil)) ; nothing more to resolve, return failure
((null a) (let ((next (litresolve orig_a (cdr b) orig_a))) ; finished one iteration of a
(list (car next) (cons (car b) (cadr next))))) ; add (car b) after recursion
((negate (car a) (car b)) ; a negates b!
(cond ((hasnegate (append (removelist (car a) orig_a) (cdr b))) ; any more negations?
(list nil nil)) ; if so, this is a vacuous truth; fail.
(t (list t (append (removelist (car a) orig_a) ; otherwise, success!
(cdr b))))))
(t (litresolve (cdr a) b orig_a)))) ; iterate on a...
; (negate a b): given two literals, a and b, return whether a and b are
; negating literals. If they are, one must be an atom, and the other must
; be a twoelement list, with the first element as "not" and the second
; equal to the atom of the other. The function checks which one is an
; atom (if either) and if the other is a two element list matching the
; requirements.
(defun negate (a b)
(cond ((atom a) ; a is an atom
(cond ((atom b) nil) ; if b is an atom too, can't be negations
(t (and (equal (car b) 'not) (equal (cadr b) a))))) ; b = (not a)?
((equal (car a) 'not) (equal b (cadr a))) ; a = (not b)?
(t nil))) ; none of the above
# ##### Removing Duplicates ##### #
; (removedups l): given a list l, this function returns a list without
; any duplicates. In the context of this program, it runs on clauses to
; make sure that a literal doesn't appear in the clause twice. (If it does,
; even if it gets removed via resolution, it will still show up, which is
; not what we want.) It runs recursively on each element on the list,
; removing anything equivalent in the rest of the list before recurring.
(defun removedups (l)
(cond ((null l) nil)
(t (cons (car l) (removedups (removelist (car l) (cdr l)))))))
; (removelist v l): given a value v and a list l, return l with all
; instances of v removed. This function looks a lot like the builtin
; remove, but because it uses the "equal" predicate, v can be a list
; (e.g., "(not a)").
(defun removelist (v l)
(cond ((null l) nil)
((equal v (car l)) (removelist v (cdr l)))
(t (cons (car l) (removelist v (cdr l))))))
; (removecaddrdups l): given a list l, this funtion returns l without any
; duplicates, where duplicates are elements whose caddr (third element) are
; equivalent. It and removecaddr below look identical to removedups and
; removelist above, except for the equivalency check, which is handled
; by listequal.
; Note: though this function works generally on a list of lists with at
; least three elements (where the third element is another list), it is
; used specifically to prune out equivalent elements in the priority queue
; in proveaux. Because the clauses of the nodes in that queue can't easily
; be sorted, the equivalency check checks to see if both elements are
; subsets of each other. Finally, because l is a priority queue, if we
; find something equivalent to (car l) later in the list, it cannot
; possibly be a better node than (car l). They must have the same hcost
; because they are identical, and (car l) has a better or equal fcost, so
; it must also have a better or equal gcost. Therefore, we should always
; keep (car l) and remove the other duplicate. We need not compare the
; costs of the two to see which will lead us to a more optimal solution.
(defun removecaddrdups (l)
(cond ((null l) nil)
(t (cons (car l) (removecaddrdups (removecaddr (car l) (cdr l)))))))
; (removecaddr v l): given a value v and a list l, where v is a list of
; length at least three (with the third element as another list) and l
; a list of values with the same properties, return a list equivalent to l
; but with each element whose third element is equivalent to v's third
; element removed.
(defun removecaddr (v l)
(cond ((null l) nil)
((listequal (third v) (third (car l)))
(removecaddr v (cdr l)))
(t (cons (car l) (removecaddr v (cdr l))))))
; (listequal l1 l2): given two lists, return whether the lists have
; identical elements, regardless of the order of those elements. It
; just checks if each is a subset of the other.
(defun listequal (l1 l2)
(and (listsubset l1 l2) (listsubset l2 l1)))
; (listsubset l1 l2): given two lists l1 and l2, return whether l1 is a
; subset of l2, i.e., if each member of l1 is in l2.
(defun listsubset (l1 l2)
(cond ((null l1) t)
((listmember (car l1) l2) (listsubset (cdr l1) l2))
(t nil)))
; (listmember v l): given a value v and a list l, return whether v is a
; member of l. This function works much like the builtin "member"
; predicate, except that it works even when v is a list (e.g., "(not a)").
(defun listmember (v l)
(cond ((null l) nil)
((equal v (car l)) t)
(t (listmember v (cdr l)))))
# ##### Other Pruning Events ##### #
; The two negation functions are based on a conversation I had with Sam
; Luckenbill about whether two clauses of the form (a (not b) c) and
; ((not a) b d) can be resolved in two different ways: to (b (not b) c d)
; and (a (not a) c d). We concluded that both of these cases lead to
; vacuous truths, so we throw out both.
; (hasnegate l): given a list l, return whether l contains any symbol and
; its negation. It runs recursively on each element in l, running
; hasunitnegate to determine if a negation exists between the element
; in l and the rest of l.
(defun hasnegate (l)
(cond ((null l) nil)
((hasunitnegate (car l) (cdr l)) t)
(t (hasnegate (cdr l)))))
; (hasunitnegate v l): given a value v and a list l, return whether l
; contains the negation of v. This function runs recursively on l, checking
; if that element is the negation of v.
(defun hasunitnegate (v l)
(cond ((null l) nil)
((negate v (car l)) t)
(t (hasunitnegate v (cdr l)))))
; (dropbig l n): given a list of clause nodes l and a maximum fcost n,
; return l without any node whose fcost is greater than n (see proveaux).
; Because the list is ordered by fcost already, as soon as we find one
; node with an fcost that is too high, the rest of the nodes will also
; have toohigh fcosts, so we just return nil.
(defun dropbig (l n)
(cond ((null l) nil) ; no more nodes
((> (+ (car (car l)) (length (third (car l)))) n) nil) ; too high, we're done
(t (cons (car l) (dropbig (cdr l) n))))) ; a good node, keep going
# ##### Sorting ##### #
; (reversecarsort l): given a list l, whose elements are lists with
; numerical first elements, this function returns l sorted in reverse order
; by the car of each element. It is a standard insertion sort using the
; auxiliary function carinsert.
(defun reversecarsort (l)
(cond ((null l) nil)
(t (carinsert (car l) (reversecarsort (cdr l))))))
; (carinsert v l): given a value v and a sorted list l, where v is a list
; whose first element is a number, and where every element of l has the
; same property, insert v into l such that no element ahead of v has
; a greater or equal first element.
(defun carinsert (v l)
(cond ((null l) (list v))
((>= (car v) (car (car l))) (cons v l))
(t (cons (car l) (carinsert v (cdr l))))))
; (addsort l): given a list of clause nodes l, run a standard insertion
; sort on them, where equivalence is determined by fcost (see proveaux).
; It uses the auxiliary function addinsert.
(defun addsort (l)
(cond ((null l) nil)
(t (addinsert (car l) (addsort (cdr l))))))
; (addinsert v l): given a value v and a sort list l, where v and every
; element of l are clause nodes (see buildds), insert v into l such that
; no element ahead of v has a smaller or equal fcost.
(defun addinsert (v l)
(cond ((null l) (list v))
((<= (+ (car v) (length (third v))) ; calculate fcost...
(+ (car (car l)) (length (third (car l)))))
(cons v l))
(t (cons (car l) (addinsert v (cdr l))))))
; (mergenodes l1 l2): given two lists of clause nodes, already sorted by
; lowest fcost, return a single list with the two lists merged and still
; sorted. The function is the latter half of a standard mergesort (without
; the initial splitting), and prefers the elements in the second list in
; case of equality. (In context, this means that it prefers to add new
; clauses to the priority queue before old clauses, since the new clauses
; are more likely to be part of a useful resolution chain.)
(defun mergenodes (l1 l2)
(cond ((null l1) l2) ; no more of l1 to merge
((null l2) l1) ; no more of l2 to merge
((< (+ (car (car l1)) (length (third (car l1)))) ; (car l1) is better
(+ (car (car l2)) (length (third (car l2)))))
(cons (car l1) (mergenodes (cdr l1) l2))) ; so add it first
(t (cons (car l2) (mergenodes l1 (cdr l2)))))) ; else, add (car l2) first