#+Title: Symbolic SAT Solver #+AUTHOR: Samuel W. Flint #+EMAIL: swflint@flintfam.org #+DATE: <2018-03-17 Sat 15:35> #+INFOJS_OPT: view:info toc:nil path:http://flintfam.org/org-info.js #+OPTIONS: toc:nil H:5 ':t *:t todo:nil stat:nil d:nil #+PROPERTY: header-args :noweb no-export :comments noweb #+LATEX_HEADER: \usepackage[margins=0.75in]{geometry} #+LATEX_HEADER: \parskip=5pt #+LATEX_HEADER: \parindent=0pt #+LATEX_HEADER: \lstset{texcl=true,breaklines=true,columns=fullflexible,basicstyle=\ttfamily,frame=lines,literate={<=}{$\leq$}1 {>=}{$\geq$}1} #+LATEX_CLASS_OPTIONS: [10pt,twoside] #+LATEX_HEADER: \pagestyle{headings} * Export :noexport: #+Caption: Export Document #+Name: export-document #+BEGIN_SRC emacs-lisp :exports none :results none (save-buffer) (let ((org-confirm-babel-evaluate (lambda (lang body) (declare (ignorable lang body)) nil))) (org-latex-export-to-pdf)) #+END_SRC * Tangle :noexport: #+Caption: Tangle Document #+Name: tangle-document #+BEGIN_SRC emacs-lisp :exports none :results none (save-buffer) (let ((python-indent-offset 4)) (org-babel-tangle)) #+END_SRC * DONE Introduction :nonum: CLOSED: [2018-03-17 Sat 23:00] The following describes and implements a SAT solver for the five most common logical connectives ($\{\lnot, \land, \lor, \Rightarrow, \Leftrightarrow\}$). It does so using the Tree Rules for Sentential Logic as described in \cite{klenk08:_under_symbol_logic}. While it is written first and foremost for programmers and computer scientists, it's also an attempt at a well-documented program that would likely be of interest to logicians who seek to understand more about the actual construction of computer programs. The organization is as follows: 1. Description and implementation of the Solver. Although this builds on things defined later, this section is the bulk of the document and also the most interesting. 2. A definition of an Expression Classifier. This is used by the solver to help decide what steps to make as it attempts to solve a given instance of the SAT problem. 3. A description of several utilities used in the Solver. These utilities are not particularly interesting, but do help to abstract away certain common tasks used in the main solver. 4. A description of how the software is packaged as a library. This in and of itself is rather mundane, however it should help to further demonstrate the organization of software. This SAT solver is written in a language called Common Lisp (\cite{pitmann05:_common_lisp_hyper}), known well in the AI community. For those unfamiliar, aside from the previously cited source several good resources are available (\cite{common_lisp_wikib,seibel05:_pract_common_lisp}). * TOC :ignore: #+TOC: headlines 3 #+TOC: listings * WORKING Solver [1/2] :PROPERTIES: :ID: 0883718a-8b30-4646-a496-9a67eb9d876c :END: The solver itself is composed of two components, the driver and expression handlers. The driver is used to dispatch based on the type of expression for expressions that have yet to be handled, and expression handlers actually deal with the expressions #+Caption: Solver #+Name: solver #+BEGIN_SRC lisp :tangle "solver.lisp" (in-package #:symbolic-sat) <> <> #+END_SRC ** DONE Driver CLOSED: [2018-03-18 Sun 10:14] :PROPERTIES: :ID: d448fc32-6def-404b-a2b1-23f74dd28a40 :END: The driver itself is a simple shim on top of the handler dispatch facility. As such, it takes an expression, adds the expression to a new list (the unhandled expressions list), and creates another list (the current path). #+Caption: Driver #+Name: driver #+BEGIN_SRC lisp (defun solve (expression) (dispatch-solution (non-atomic-add expression (list)) (list expression))) #+END_SRC ** WORKING Expression Handlers [0/7] :PROPERTIES: :ID: 99e68a1a-b3a4-40c5-9b2e-92d5e976d5bb :END: This is organized as follows: handler storage, a recipe for handler definition, handler dispatch and the the definition of the handlers themselves. #+Caption: Expression Handlers #+Name: expression-handlers #+BEGIN_SRC lisp (defvar *handlers* '()) <> <> <> <> <> <> <> #+END_SRC *** TODO Defining Handlers :PROPERTIES: :ID: 2a90b9c3-585e-4347-89d7-78035e88e681 :END: #+Caption: Defining Handlers #+Name: defining-handlers #+BEGIN_SRC lisp (defmacro define-expression-handler (expression-type &body handler) (let ((name (symbolicate 'handle- expression-type))) `(progn (defun ,name (expression unchecked current-path) ,@handler) (pushnew '(,expression-type . ,name) *handlers* :key #'first) ',expression-type))) #+END_SRC *** TODO Dispatching Handlers :PROPERTIES: :ID: c4a9936b-d87a-4f78-87ef-fb81238cc41c :END: #+Caption: Dispatching Handlers #+Name: dispatching-handlers #+BEGIN_SRC lisp (defun dispatch-solution (unchecked current-path) (if (null unchecked) (collect-atoms current-path) (let ((expression (first unchecked)) (unchecked (rest unchecked))) (do* ((pair (first *handlers*) (first remaining)) (remaining (rest *handlers*) (rest remaining))) ((or (null pair) (expression-type-p (car pair) expression)) (when (not (null pair)) (funcall (cdr pair) expression unchecked current-path))))))) #+END_SRC *** TODO And :PROPERTIES: :ID: e630fba3-005d-474e-88e5-0acb61f66ab1 :END: #+Caption: And Handlers #+Name: and-handlers #+BEGIN_SRC lisp (define-expression-handler sentential-and (when (not (any-conflict-p (rest expression) current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms (rest expression)) unchecked) (concatenate 'list (rest expression) current-path)))) (define-expression-handler not-and (let ((expr-list (map 'list (lambda (expr) `(not ,expr)) (rest (second expression)))) (satp nil)) (do* ((expr-prime (first expr-list) (first expr-list-prime)) (expr-list-prime (rest expr-list) (rest expr-list-prime))) ((or satp (null expr-prime)) satp) (when (not (has-conflict-p expr-prime current-path)) (setf satp (dispatch-solution (non-atomic-add expr-prime unchecked) (cons expr-prime current-path))))))) #+END_SRC *** TODO Or :PROPERTIES: :ID: e148ef8b-8287-4930-a489-187fea5a63c0 :END: #+Caption: Or Handlers #+Name: or-handlers #+BEGIN_SRC lisp (define-expression-handler sentential-or (let ((satp nil)) (do ((expr (first (rest expression)) (first expr-list)) (expr-list (rest (rest expression)) (rest expr-list))) ((or satp (null expr)) satp) (when (not (has-conflict-p expr current-path)) (setf satp (dispatch-solution (non-atomic-add expr unchecked) (cons expr current-path))))))) (define-expression-handler not-or (let ((expr-list (map 'list (lambda (expr) `(not ,expr)) (rest (second expression))))) (when (not (any-conflict-p expr-list current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms expr-list) unchecked) (concatenate 'list expr-list current-path))))) #+END_SRC *** TODO Implication :PROPERTIES: :ID: a2eb81f5-c834-4529-b367-f618e877a817 :END: #+Caption: Implication Handlers #+Name: implication-handlers #+BEGIN_SRC lisp (define-expression-handler sentential-implication (let ((branch-a `(not ,(second expression))) (branch-b (third expression))) (cond ((not (has-conflict-p branch-a current-path)) (dispatch-solution (non-atomic-add branch-a unchecked) (cons branch-a current-path))) ((not (has-conflict-p branch-b current-path)) (dispatch-solution (non-atomic-add branch-b unchecked) (cons branch-b current-path))) (t nil)))) (define-expression-handler not-implication (let ((the-expr-list (list (second (second expression)) `(not ,(third (second expression)))))) (when (not (any-conflict-p the-expr-list current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms the-expr-list) unchecked) (concatenate 'list the-expr-list current-path))))) #+END_SRC *** TODO Biconditional :PROPERTIES: :ID: 3a765282-de1f-450b-8d45-e3cf270886d0 :END: #+Caption: Biconditional #+Name: biconditional-handlers #+BEGIN_SRC lisp (define-expression-handler sentential-biconditional (let* ((branch-a (rest expression)) (branch-b (map 'list (lambda (expr) `(not ,expr)) branch-a))) (cond ((not (any-conflict-p branch-a current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms branch-a) unchecked) (concatenate 'list branch-a current-path))) ((not (any-conflict-p branch-b current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms branch-b) unchecked) (concatenate 'list branch-b current-path))) (t nil)))) (define-expression-handler not-biconditional (let ((branch-a (list (second (second expression)) `(not ,(third (second expression))))) (branch-b (list `(not ,(second (second expression))) (third (second expression))))) (cond ((not (any-conflict-p branch-a current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms branch-a) unchecked) (concatenate 'list branch-a current-path))) ((not (any-conflict-p branch-b current-path)) (dispatch-solution (concatenate 'list (collect-non-atoms branch-b) unchecked) (concatenate 'list branch-b current-path))) (t nil)))) #+END_SRC *** TODO Doubled Not :PROPERTIES: :ID: 2edb4da5-08f1-430c-b96b-c96628805602 :END: #+Caption: Doubled Not Handler #+Name: doubled-not-handler #+BEGIN_SRC lisp (define-expression-handler double-not (let ((new (second (second expression)))) (dispatch-solution (non-atomic-add new unchecked) (cons new current-path)))) #+END_SRC * WORKING Expression Classification [0/8] :PROPERTIES: :ID: 98ce9388-02b2-4027-aa4e-0a82ef8e3cbd :END: #+Caption: Expression Classification #+Name: expression-classification #+BEGIN_SRC lisp :tangle "classifier.lisp" (in-package #:symbolic-sat-classifier) (defvar *types* '()) <> <> <> <> <> <> <> <> #+END_SRC ** TODO Expression Type Definition #+Caption: Expression Type Definition #+Name: expression-type-definition #+BEGIN_SRC lisp (defmacro define-expression-type (type-name &rest predicate) (check-type type-name symbol) (let ((predicate-name (symbolicate type-name '-p))) `(progn (defun ,predicate-name (expression) ,@predicate) (pushnew '(,type-name . ,predicate-name) *types* :key #'first :test #'equal) (export ',type-name) ',type-name))) #+END_SRC ** TODO Expresion Type Checking #+Caption: Expression Type Checking #+Name: expression-type-checking #+BEGIN_SRC lisp (defun expression-type-p (expression-type expression) (if (eq '* expression-type) t (funcall (cdr (assoc expression-type *types*)) expression))) #+END_SRC ** TODO Not :PROPERTIES: :ID: 4884bd62-39d8-487e-9b1d-36cb1a6b8372 :END: #+Caption: Not Classification #+Name: not-classification #+BEGIN_SRC lisp (define-expression-type sentential-not (and (listp expression) (equal (first expression) 'not) (= (length expression) 2))) (define-expression-type double-not (and (expression-type-p 'sentential-not expression) (listp (second expression)) (expression-type-p 'sentential-not (second expression)))) #+END_SRC ** TODO And :PROPERTIES: :ID: 3ab30c56-7eda-4bb5-8e17-aa49587d7b81 :END: #+Caption: And Classification #+Name: and-classification #+BEGIN_SRC lisp (define-expression-type sentential-and (and (listp expression) (equal (first expression) 'and) (>= (length (rest expression)) 2))) (define-expression-type not-and (and (expression-type-p 'sentential-not expression) (listp (second expression)) (expression-type-p 'sentential-and (second expression)))) #+END_SRC ** TODO Or :PROPERTIES: :ID: d3c68b18-5f67-452c-ae9b-44285affe2a3 :END: #+Caption: Or Classification #+Name: or-classification #+BEGIN_SRC lisp (define-expression-type sentential-or (and (listp expression) (equal (first expression) 'or) (>= (length (rest expression)) 2))) (define-expression-type not-or (and (expression-type-p 'sentential-not expression) (listp (second expression)) (expression-type-p 'sentential-or (second expression)))) #+END_SRC ** TODO Implication :PROPERTIES: :ID: 5df00489-662d-4579-b665-3e381113958d :END: #+Caption: Implication Classification #+Name: implication-classification #+BEGIN_SRC lisp (define-expression-type sentential-implication (and (listp expression) (equal 'implies (first expression)) (= (length (rest expression)) 2))) (define-expression-type not-implication (and (expression-type-p 'sentential-not expression) (listp (second expression)) (expression-type-p 'sentential-implication (second expression)))) #+END_SRC ** TODO Biconditional :PROPERTIES: :ID: a390b595-f794-4b1d-8233-376fc704c85c :END: #+Caption: Biconditional Classification #+Name: bicond-classification #+BEGIN_SRC lisp (define-expression-type sentential-biconditional (and (listp expression) (equal (first expression) 'iff) (= (length (rest expression)) 2))) (define-expression-type not-biconditional (and (expression-type-p 'sentential-not expression) (listp (second expression)) (expression-type-p 'sentential-biconditional (second expression)))) #+END_SRC ** TODO Other :PROPERTIES: :ID: f80903bd-0afe-40fd-9c2f-48d458393483 :END: #+Caption: Atom Classification #+Name: atom-classification #+BEGIN_SRC lisp (define-expression-type atom (or (symbolp expression) (and (expression-type-p 'sentential-not expression) (symbolp (second expression))))) #+END_SRC * TODO Utilities :PROPERTIES: :ID: 1c6e6f57-1c3e-4a9f-bd08-6223fc83e4f9 :END: #+Caption: Utilities #+Name: utils #+BEGIN_SRC lisp :tangle "utils.lisp" (in-package #:symbolic-sat-utils) <> <> <> #+END_SRC ** TODO Clause Collection :PROPERTIES: :ID: e93d0557-17ca-44a0-8ac8-23ef8db84272 :END: #+Caption: Clause Collection #+Name: clause-collection #+BEGIN_SRC lisp (defun collect-atoms (expr-list) (remove-duplicates (remove-if (lambda (expr) (not (expression-type-p 'atom expr))) expr-list) :test #'equal)) (defun collect-non-atoms (expr-list) (remove-duplicates (remove-if (lambda (expr) (expression-type-p 'atom expr)) expr-list) :test #'equal)) #+END_SRC ** TODO Conflict Checking :PROPERTIES: :ID: cbb3a699-83af-460c-a6b0-dcb7f1ca9aef :END: #+Caption: Conflict Checking #+Name: conflict-checking #+BEGIN_SRC lisp (defun has-conflict-p (current path) (or (member `(not ,current) path :test #'equal) (and (expression-type-p 'sentential-not current) (member (second current) path :test #'equal)))) (defun any-conflict-p (expr-list path) (do* ((expr (first expr-list) (first expr-list-prime)) (expr-list-prime (rest expr-list) (rest expr-list-prime))) ((or (has-conflict-p expr path) (null expr)) (when (not (null expr)) t)))) #+END_SRC ** TODO Clause Adding :PROPERTIES: :ID: 2cf45428-0740-4b08-bba8-68353a9b79f3 :END: #+Caption: Clause Adding #+Name: clause-adding #+BEGIN_SRC lisp (defun non-atomic-add (expr list) (if (not (expression-type-p 'atom expr)) (cons expr list) list)) #+END_SRC * TODO Packaging :PROPERTIES: :ID: ca73d4ab-45ba-4e7c-819a-b87d6a529083 :END: ** TODO Package Definition :PROPERTIES: :ID: 3ac44dcd-3417-4b45-819c-54bef90f8145 :END: #+Caption: Package Definitions #+Name: package-definitions #+BEGIN_SRC lisp :tangle "packages.lisp" (defpackage #:symbolic-sat-common-symbols (:use #:cl) (:export #:implies #:iff)) (defpackage #:symbolic-sat-classifier (:use #:cl #:symbolic-sat-common-symbols) (:import-from #:alexandria #:symbolicate) (:export #:expression-type-p)) (defpackage #:symbolic-sat-utils (:use #:cl #:symbolic-sat-common-symbols #:symbolic-sat-classifier) (:export #:collect-atoms #:collect-non-atoms #:has-conflict-p #:any-conflict-p #:non-atomic-add)) (defpackage #:symbolic-sat (:use #:cl #:symbolic-sat-classifier #:symbolic-sat-common-symbols #:symbolic-sat-utils) (:import-from #:alexandria #:symbolicate) (:export #:solve)) #+END_SRC ** TODO System Definition :PROPERTIES: :ID: f0b739ff-07ef-4322-93f3-5dced945540e :END: #+Caption: System Definition #+Name: system-definition #+BEGIN_SRC lisp :tangle "symbolic-sat.asd" (asdf:defsystem #:symbolic-sat :description "A basic Symbolic SAT solver using the Tableaux (tree) method for Sentential Logic." :author "Samuel Flint " :license "GNU GPLv3 or Later" :depends-on (#:alexandria) :serial t :components ((:file "packages") (:file "classifier") (:file "utils") (:file "solver"))) #+END_SRC * Bibliography :ignore: \bibliographystyle{plain} \bibliography{bibliography}