symbolic-sat/symbolic-sat.org

Symbolic SAT Solver

Introduction

TOC   ignore

Expression Classification

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

Not

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

And

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

Or

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

Implication

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

Biconditional

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

Other

  (define-expression-type atom
      (or (symbolp expression)
         (and (expression-type-p 'sentential-not expression)
            (symbolp (second expression)))))

Driver

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

Expression Handlers

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

And

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

Or

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

Implication

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

Biconditional

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

Doubled Not

  (define-expression-handler double-not
    (let ((new (second (second expression))))
      (solve-it (non-atomic-add new unchecked) (cons new current-path))))

Utilities

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

Packaging

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