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

* TODO Introduction

* 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
  (defvar *expression-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) *expression-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 *expression-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 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 *expression-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) *expression-handlers* :key #'first)
         ',expression-type)))

  (defun dispatch-on (expression unchecked current-path)
    (do* ((pair (first *expression-handlers*) (first remaining))
          (remaining (rest *expression-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-close (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 (close-tree-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 (close-tree-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-close 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 (close-tree-p branch-a current-path))
         (solve-it (non-atomic-add branch-a unchecked) (cons branch-a current-path)))
        ((not (close-tree-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-close 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-close branch-a current-path))
         (solve-it (concatenate 'list (collect-non-atoms branch-a) unchecked)
                   (concatenate 'list branch-a current-path)))
        ((not (any-close 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-close branch-a current-path))
         (solve-it (concatenate 'list (collect-non-atoms branch-a) unchecked)
                   (concatenate 'list branch-a current-path)))
        ((not (any-close 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

#+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 
  (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 close-tree-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-close (expr-list path)
    (do* ((expr (first expr-list) (first expr-list-prime))
          (expr-list-prime (rest expr-list) (rest expr-list-prime)))
         ((or (close-tree-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:

#+Caption: Packaging
#+Name: packaging
#+BEGIN_SRC lisp :tangle "symbolic-sat.lisp"
  (ql:quickload :alexandria)

  (defpackage #:symbolic-sat
    (:use #:cl)
    (:import-from #:alexandria
                  #:symbolicate)
    (:export #:expression-type-p
             #:implies
             #:iff
             #:solve))

  (in-package #:symbolic-sat)

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