#+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

* TODO Expression Classification
: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* '())

  (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)))

  (defun expression-type-p (expression-type expression)
    (if (eq '* expression-type)
        t
        (funcall (cdr (assoc expression-type *types*))
                 expression)))

  <<not-classification>>
  <<and-classification>>
  <<or-classification>>
  <<implication-classification>>
  <<bicond-classification>>
  <<atom-classification>>
#+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 Solver
:PROPERTIES:
:ID:       0883718a-8b30-4646-a496-9a67eb9d876c
:END:

#+Caption: Solver
#+Name: solver
#+BEGIN_SRC lisp :tangle "solver.lisp"
  (in-package #:symbolic-sat)

  <<expression-handlers>>
  <<driver>>
#+END_SRC

** TODO Driver
:PROPERTIES:
:ID:       d448fc32-6def-404b-a2b1-23f74dd28a40
:END:

#+Caption: Driver
#+Name: driver
#+BEGIN_SRC lisp 
  (defun solve-it (unchecked current-path)
    (if (null unchecked)
        (collect-atoms current-path)
        (dispatch-on (first unchecked)
                     (rest unchecked)
                     current-path)))

  (defun solve (expression)
    (solve-it (list expression)
              (list expression)))
#+END_SRC

** TODO Expression Handlers
:PROPERTIES:
:ID:       99e68a1a-b3a4-40c5-9b2e-92d5e976d5bb
:END:

#+Caption: Expression Handlers
#+Name: expression-handlers
#+BEGIN_SRC lisp 
  (defvar *handlers* '())

  (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)))

  (defun dispatch-on (expression unchecked current-path)
    (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)))))

  <<and-handlers>>
  <<or-handlers>>
  <<implication-handlers>>
  <<biconditional-handlers>>
  <<doubled-not-handler>>
#+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))
      (solve-it (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 (solve-it (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 (solve-it (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))
        (solve-it (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))
         (solve-it (non-atomic-add branch-a unchecked) (cons branch-a current-path)))
        ((not (has-conflict-p branch-b current-path))
         (solve-it (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))
        (solve-it (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))
         (solve-it (concatenate 'list (collect-non-atoms branch-a) unchecked)
                   (concatenate 'list branch-a current-path)))
        ((not (any-conflict-p branch-b current-path))
         (solve-it (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))
         (solve-it (concatenate 'list (collect-non-atoms branch-a) unchecked)
                   (concatenate 'list branch-a current-path)))
        ((not (any-conflict-p branch-b current-path))
         (solve-it (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))))
      (solve-it (non-atomic-add new unchecked) (cons new current-path))))
#+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)

  (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))

  (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))))

  (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 <swflint@flintfam.org>"
    :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}