#+Title: Symbolic SAT Solver
#+AUTHOR: Samuel W. Flint
#+EMAIL: swflint@flintfam.org
#+DATE: \today
#+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: \lstset{texcl=true,breaklines=true,columns=fullflexible,basicstyle=\ttfamily,frame=lines,literate={<=}{$\leq$}1 {>=}{$\geq$}1}
#+LATEX_CLASS_OPTIONS: [10pt,twoside,paper=letter,DIV=14]
#+LATEX_HEADER: \usepackage[style=numeric-comp]{biblatex}
#+LATEX_HEADER: \addbibresource{bibliography.bib}
#+LATEX_HEADER: \usepackage[plextt,closedroot]{mycommon}

* 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)
  (org-babel-tangle)
#+END_SRC

* DONE Introduction                                                   :nonum:
CLOSED: [2018-03-23 Fri 21:53]

The following describes and implements a SAT solver for the five most common logical connectives ($\{\lnot, \land, \lor, \Rightarrow, \Leftrightarrow\}$) without requiring an expression to be in a specific normal form.  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.

Because of the nature of the problem at hand, this is written using the Common Lisp language [[cite:CommonLi93:online]], which is known in the Artificial Intelligence community.  It was chosen for three primary reasons: a) the author's familiarity; b) incredible support for symbolic processing; and c) excellent support for several forms of meta-programming, one of which (template-based meta-programming) is used in this program.  As this document is in part for those outside of programming [[cite:CommonLi95:online,seibel05:_pract_common_lisp]] provide for excelent reference, as does the above mentioned specification. 

* TOC                                                                :ignore:

#+TOC: headlines 3
#+TOC: listings

* WORKING Solver [1/2]
:PROPERTIES:
:ID:       0883718a-8b30-4646-a496-9a67eb9d876c
:END:

The solver is built primarily on three components, a driver (which is itself a shim upon a dispatcher), a dispatcher (which selects which expression handler to use based on the type of expression at hand) and expression handlers (which apply the various tree rules).

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

  <<expression-handlers>>
  <<driver>>
#+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)
    (let ((solution (dispatch-solution (non-atomic-add expression (list))
                                       (list expression))))
      (when (not (null solution))
        (sort-atoms solution))))
#+END_SRC

** WORKING Expression Handlers [2/8]
: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* '())

  <<defining-handlers>>

  <<pick-next-expression>>

  <<dispatching-handlers>>

  <<and-handlers>>
  <<or-handlers>>
  <<implication-handlers>>
  <<biconditional-handlers>>
  <<doubled-not-handler>>
#+END_SRC

*** DONE Defining Handlers
CLOSED: [2018-03-23 Fri 21:47]
:PROPERTIES:
:ID:       2a90b9c3-585e-4347-89d7-78035e88e681
:END:

This macro (~define-expression-handler~) takes two arguments, an expression type and a handler body.  It uses the type to create a name for the handler itself, and the defines a function with that name, taking three arguments: the current expression, the list of unchecked expressions and the current path.  It then places the handler body in the function, pushes a single cell of the expression type and the handler name onto the handler storage list, and returns the expression type.

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

*** DONE Dispatching Handlers
CLOSED: [2018-03-23 Fri 21:59]
:PROPERTIES:
:ID:       c4a9936b-d87a-4f78-87ef-fb81238cc41c
:END:

These 11 lines are the most important in the application.  This is what's used to cause a handler to be selected and called, or to decide if a solution has been found.  This is done by first checking if the list of unchecked expressions is empty, and if so, simply collecting all atoms in the current path.  Otherwise, it takes the top expression from ~unchecked~, and rebinds ~unchecked~ to the rest of itself, and then looks for a handler.  This is done by looking at those available, and if the current expression is of the given type, ending by applying that handler to the current expression.

#+Caption: Dispatching Handlers
#+Name: dispatching-handlers
#+BEGIN_SRC lisp 
  (defun dispatch-solution (unchecked current-path)
    (if (null unchecked)
        (collect-atoms current-path)
        (multiple-value-bind (expression unchecked) (pick-next-expression 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 Pick Next Expression
:PROPERTIES:
:ID:       80b62141-8f31-4528-95a1-63c014936932
:END:

#+Caption: Pick Next Expression
#+Name: pick-next-expression
#+BEGIN_SRC lisp 
  (defun pick-next-expression (unchecked-expressions)
    (let (next-expression)
      (do ((branchiness 0 (1+ branchiness)))
          ((or (not (null next-expression))
              (> branchiness 2)))
        (setf next-expression (first (remove-if (complement (is-branchy-as branchiness)) unchecked-expressions))))
      (values next-expression (remove next-expression unchecked-expressions :test #'equal))))
#+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 [3/9]
:PROPERTIES:
:ID:       98ce9388-02b2-4027-aa4e-0a82ef8e3cbd
:END:

For the solver to work correctly, it needs to decide what kind of expressions it's looking at.  To do that, it uses a few relatively simple tests to choose or determine expression type.  These are defined here.

#+Caption: Expression Classification
#+Name: expression-classification
#+BEGIN_SRC lisp :tangle "classifier.lisp"
  (in-package #:symbolic-sat-classifier)

  (defvar *types* '())

  <<expression-type-definition>>

  <<expression-type-checking>>

  <<expression-branchiness-check>>

  <<not-classification>>
  <<and-classification>>
  <<or-classification>>
  <<implication-classification>>
  <<bicond-classification>>
  <<atom-classification>>
#+END_SRC

** DONE Expression Type Definition
CLOSED: [2019-07-12 Fri 13:19]
:PROPERTIES:
:ID:       62fee56e-3f7c-4575-a870-326a53e939d4
:END:

To even be able to check types, we need to define types.  This is done with the ~define-expression-type~ macro, which takes the name of the type, its "branchiness" (more on that in other sections), and a predicate body.  It expands to define the predicate, updates the types list with relevant information (name, predicate name, branchiness), and exports the type name from the package (making it available to others).

#+Caption: Expression Type Definition
#+Name: expression-type-definition
#+BEGIN_SRC lisp 
  (defmacro define-expression-type (type-name branchiness &body predicate)
    (check-type type-name symbol)
    (check-type branchiness integer)
    (let ((predicate-name (symbolicate type-name '-p)))
      `(progn
         (defun ,predicate-name (expression)
           ,@predicate)
         (pushnew '(,type-name ,predicate-name ,branchiness) *types* :key #'first :test #'equal)
         (export ',type-name)
         ',type-name)))
#+END_SRC

** DONE Expression Type Checking
CLOSED: [2019-07-12 Fri 13:56]
:PROPERTIES:
:ID:       34540858-636e-4336-89e7-63dca947c739
:END:

Expressions are checked for their type with ~expression-type-p~, which takes a type name (either ~*~ or one that's defined later on), and an expression.  If the type name is simply ~*~, it returns true.  Otherwise, it looks for the type predicate (using ~assoc~), and calls it (the second value in the three-tuple ~*types*~ entry) on the expression.

#+Caption: Expression Type Checking
#+Name: expression-type-checking
#+BEGIN_SRC lisp 
  (defun expression-type-p (expression-type expression)
    (if (eq '* expression-type)
        t
        (funcall (second (assoc expression-type *types*))
                 expression)))
#+END_SRC

** DONE Check Branchiness
CLOSED: [2019-07-12 Fri 14:13]
:PROPERTIES:
:ID:       5c404f5f-0782-460e-bb57-a6222977bd1a
:END:

An expression's "branchiness" is a value that (generally) is in the range \([-1, 2]\) (with some outliers for things that are used as helper types).  This tells the algorithm how likely an expression is to create branches in the tree.  To be able to use this, we have two functions: ~has-branchiness-p~ and ~is-branchy-as~.

~has-branchiness-p~ operates by first finding the predicates for types with the given ~branchiness~.  It then goes through these tests, one-by-one, returning the type entry if it passes, going on to the next otherwise.  If eventually the test object itself is simply ~nil~, it terminates, letting us know that the ~expression~ does not have the given ~branchiness~ value.

~is-branchy-as~ works as a wrapper to create functions that can be used in various filtering functions (~remove-if~, /etc./).

#+Caption: Check Expression Branchiness
#+Name: expression-branchiness-check
#+BEGIN_SRC lisp 
  (defun has-branchiness-p (branchiness expression)
    (let ((tests (remove-if (lambda (x) (/= branchiness x)) *types* :key #'third)))
      (do* ((test (first tests) (first tests-prime))
            (tests-prime (rest tests) (rest tests-prime)))
           ((or (null test)
               (funcall (second test) expression))
            test))))

  (defun is-branchy-as (branchiness)
    (lambda (expression)
      (has-branchiness-p branchiness 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 5
    (and (listp expression)
       (equal (first expression) 'not)
       (= (length expression) 2)))

  (define-expression-type double-not 0
    (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 1
    (and (listp expression)
       (equal (first expression) 'and)
       (>= (length (rest expression)) 2)))

  (define-expression-type not-and 2
    (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 2
    (and (listp expression)
       (equal (first expression) 'or)
       (>= (length (rest expression)) 2)))

  (define-expression-type not-or 1
    (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 2
    (and (listp expression)
       (equal 'implies (first expression))
       (= (length (rest expression)) 2)))

  (define-expression-type not-implication 1
    (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 2
    (and (listp expression)
       (equal (first expression) 'iff)
       (= (length (rest expression)) 2)))

  (define-expression-type not-biconditional 2
    (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 -1
    (or (symbolp expression)
       (and (expression-type-p 'sentential-not expression)
          (symbolp (second expression)))))
#+END_SRC

* WORKING Utilities [1/4]
:PROPERTIES:
:ID:       1c6e6f57-1c3e-4a9f-bd08-6223fc83e4f9
:END:

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

  <<expression-collection>>
  <<conflict-checking>>
  <<expression-adding>>
  <<sort-atoms>>
#+END_SRC

** TODO Expression Collection
:PROPERTIES:
:ID:       e93d0557-17ca-44a0-8ac8-23ef8db84272
:END:

#+Caption: Expression Collection
#+Name: expression-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))
          (not (null expr)))))
#+END_SRC

** DONE Expression Adding
CLOSED: [2019-07-12 Fri 14:18]
:PROPERTIES:
:ID:       2cf45428-0740-4b08-bba8-68353a9b79f3
:END:

To simplify some things in the solver (adding expressions to the list of unchecked), we take an expression, and a list of other expressions.  If the expression is not an ~atom~ (recall the various types), it ~cons~'s it on to the front of the list, or returns just the list with no modifications.

#+Caption: Expression Adding
#+Name: expression-adding
#+BEGIN_SRC lisp 
  (defun non-atomic-add (expr list)
    (if (not (expression-type-p 'atom expr))
        (cons expr list)
        list))
#+END_SRC

** TODO Sort Atoms
:PROPERTIES:
:ID:       5cdb7bfe-eba9-4d26-b7ac-a8aa9eea2280
:END:

#+Caption: Sort Atoms
#+Name: sort-atoms
#+BEGIN_SRC lisp 
  (defun sort-atoms (atoms-list)
    (flet ((atom-less-than-p (atom-a atom-b)
             (let ((aa (if (atom atom-a) atom-a (second atom-a)))
                   (ab (if (atom atom-b) atom-b (second atom-b))))
               (string<= (format nil "~A" aa)
                         (format nil "~A" ab)))))
      (sort atoms-list #'atom-less-than-p)))
#+END_SRC

* DONE Packaging [2/2]
:PROPERTIES:
:ID:       ca73d4ab-45ba-4e7c-819a-b87d6a529083
:END:

As a software library, packaging is important.  In Common Lisp, it's done using system packages and something called ASDF (A System Definition Facility) to enable the library to be loaded correctly and quickly.

** DONE Package Definition
CLOSED: [2018-05-28 Mon 10:05]
:PROPERTIES:
:ID:       3ac44dcd-3417-4b45-819c-54bef90f8145
:END:

Symbolic SAT is composed of four packages, as follows:

 - ~symbolic-sat-common-symbols~ :: This package exports two symbols that are used and in common for all other packages.  These symbols also provide a part of the external API.
 - ~symbolic-sat-classifier~ :: This package provides an API for classifying expressions -- deciding what type of expression is at hand.  It requires the use of the Common Lisp package (providing all basic symbols as defined in the standard), and the previous common symbols package.  It also uses ~symbolicate~ from Alexandria to mash symbols together for use in automatically generated function and variable names.  It directly exports one symbol, ~expression-type-p~ which is better described in Section [[id:34540858-636e-4336-89e7-63dca947c739]].
 - ~symbolic-sat-utils~ :: Another utility package, the functions exported are well defined in Section [[id:1c6e6f57-1c3e-4a9f-bd08-6223fc83e4f9]], but it builds on the previous two packages, and exports the named symbols.
 - ~symbolic-sat~ :: This is the final package, providing perhaps, the most important part of the API, ~solve~.  It builds upon all three prior packages, and again uses ~symbolicate~ for mashing symbols together.

#+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
             #:has-branchiness-p
             #:is-branchy-as))

  (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
             #:sort-atoms))

  (defpackage #:symbolic-sat
    (:use #:cl
          #:symbolic-sat-classifier
          #:symbolic-sat-common-symbols
          #:symbolic-sat-utils)
    (:import-from #:alexandria
                  #:symbolicate)
    (:export #:solve))
#+END_SRC

** DONE System Definition
CLOSED: [2018-05-28 Mon 10:16]
:PROPERTIES:
:ID:       f0b739ff-07ef-4322-93f3-5dced945540e
:END:

This defines the ASDF system, called ~#:symbolic-sat~, having a description, an author, and a license as properties.  It states that it depends on ~#:alexandria~, a utilities collection.  It further states that the components (as defined by the expression following ~:components~) must be loaded in that order with ~:serial t~.

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

#+LATEX: \printbibliography