Simple sat solver

dpll.rkt

#lang racket


;; Notes on CNF form:
;; A CNF formula is a list of claues. These clauses are semantically "and-ed" together
;; Each clause is a list of "literals". Each literal is semantically "or-ed" together
;; Each literal is either a positive or negative atom
;; Each atom is either "true", "false", or a variable

;; An example satisfiable formula
(define example-sat
  `(((- x1) x2 x4)
    (x1 x3)
    ((- x4) (- x2))
    ((- x4) (- x1) x2)
    (x3 (- x1))
    (x1 x4)
    ((- x2) x1)))

;; An example unsatisfiable formula
(define example-unsat
  `(((- x1) x2 x4)
    (x1 x3)
    ((- x4) (- x2))
    ((- x4) (- x1) x2)
    (x6)
    (x3 (- x1))
    (x1 x4)
    ((- x2) x1)
    ((- x6))))

;; The DPLL algorithm
;; Takes a formula and returns either
;; -- #f is the formula is unsatisifable
;; -- a hash containing a satisfying assigninment
;; This algorithm is sound and complete
(define (dpll f)
  ;; Run boolean-constraint-propagation, then check the state of the formula
  (define g (bcp f))
  (cond
    [(contradiction? g) #f]
    [(satisfied? g) (binding g)]
    ;; If the formula is neither satisfied or a contradiction
    ;; Choose a variable to assign. Start by assigning it to true.
    ;; If that doesn't work, assigned it to false (backtracking).
    [else
     (let ((p (choose (unassigned-vars g))))
       (or (dpll (bind g p #t))
           (dpll (bind g p #f))))]))


;; Choose an unassigned variable to assign
;; Any choice here is sound and complete
;; We're gonna be stupid and just pick the first one
;; In reality, you'd use some heuristic.
(define (choose lst)
  (first lst))


;; A note on the "unit clause rule". This logical rule is the heart of boolean constraint propagation.
;; Remember that literals are "or-ed" together.
;; A clause where any of the literals evaluate to true is satisifed.
;; A cluase where all of the literals evaluate to false is a contradiction.
;; A clause that is not satisfied, but exactly one variable is not yet assigned is called a unit clause.
;; This is special, because we can conclude easily what the value of that literal has to be:
;; It must evaluate to true, or else we're in a contradiction
;; This is great! Every time we make a decision, we should find all the unit clauses we can, and learn from them (create new assignments)
;; In doing that, we might create new unit clauses, so we have to keep checking in a loop until we're done

;; The boolean-constraint-propagation algorithm
;; Takes a formula, and returns a formula simplified by
;; repeatedly applying the unit-clause rule until a fixed point is reached
(define (bcp f)
  ;; Attempt to find a "unit clause"
  (match (find-unit-clause f)
    ;; If we find a contradiction -> bail out
    ['contradiction 'contradiction]
    ;; If there's no unit clauses -> we reached a fixed point
    ['none f]
    ;; If there's a unit clause, force the unit to be true then recurse
    [`(some ,unit-literal)
     (bcp (bind f
                (literal->var unit-literal)
                (literal->consequence unit-literal)))]))

;; Attempt to find a unit clause
;; Takes a formula
;; Returns one of:
;; 'contradiction - simplifying resulted in a contradiction
;; 'none - there are no unit clauses
;; '(some ,literal) - there is a unit clause and here is the unassigned literal
(define (find-unit-clause f)
  ;; This search will work by iterating through the list of clauses and checking the state of each clause
  ;; For a contradicted or unit clause, we'll raise an exception to end the search
  (with-handlers 
      [(contradiction-exception? (constant 'contradiction)) ;; If we find a contradiction return 'contradiction
       (unit-exception? (λ (exc) (list 'some (unit-exception-literal exc))))] ;; If we find a unit cluase return `(some ,unit-atom)
    (begin
      (for [(clause (clauses f))] ;; Iterate over the clauses
        (match (clause-state clause f) ;; Compute the state of the clause
          ['contradiction (raise (contradiction-exception))]
          [(list 'unit unit-literal) (raise (unit-exception unit-literal))]
          [_ (void)]))
      'none))) ;; If we get through all the clauses and only found satisfied or unassigned clauses, we're done: there are no unit clauses

;; A clause in one four states
;; - satisfied - any of the atom resolve to true
;; - contradiction - all of the atoms resolve to false
;; - unit - there is exactly one unsatisfied atom
;; - unsatisfied - other
(define (clause-state clause f)
  (define unassigned '())
  (define any-satisfied #f)
  (for [(literal clause)]
    (match (eval-literal literal f)
      [#t (set! any-satisfied #t)]
      [#f (void)]
      ['unassigned (set! unassigned (cons literal unassigned))]))
  (cond
    [any-satisfied 'satisfied]
    [(empty? unassigned) 'contradiction]
    [(= 1 (length unassigned)) (list 'unit (first unassigned))]
    [else 'unsatisfied]))

;; Evaluate a literal to a value. Will return either `#t`,`#f` or 'unassigned
(define (eval-literal literal f)
  (cond
    [(positive-literal? literal) (eval-atom (literal->atom literal) f)]
    [(negative-literal? literal) (not* (eval-atom (literal->atom literal) f))]))

;; Negate the value of an atom. Propagates 'unassigned
(define (not* x)
  (if (boolean? x)
      (not x)
      'unassigned))

;; Evaluates an atom
;; True/False literals evaluate to booleans
;; Everything else is a variable, and so is looked up in the current binding
;; This may evaluate to 'unassigned if the variable is not assigned in the current binding
(define (eval-atom atom f)
  (match atom
    ['true #t]
    ['false #f]
    [_ (lookup f atom)]))

;; A formula is a
;; | (list clauses binding vars) - representing a in progress solution
;; | 'contradiction - representing a contradiction
;; Clauses is a list of CNF clauses

;; High level operations on formulas

;; Is the current formula satisfied?
(define (satisfied? f)
  ;; It is if we have no unassigned variables left
  (empty? (unassigned-vars f)))

;; Is the current formula a contradiction?
(define (contradiction? f)
  (eq? f 'contradiction))

;; Get the list of unassigned variables in the formula
(define (unassigned-vars f)
  (filter-not (λ (x) (in-binding? f x)) (vars f)))

;; Is the variable `x` assigned in the formula `f`?
(define (in-binding? f x)
  (hash-has-key? (binding f) x))

;; Looks up the variable `x` in the binding, returning 'unassigned if not present
(define (lookup f x)
  (hash-ref (binding f) x 'unassigned))



;; Constructors for formulas

;; Constructor for in-progress formulas
(define (formula clauses binding vars)
  (list clauses binding vars))

;; Create a formula from a list of claues
(define (new-formula clauses)
  (formula clauses (empty-binding) (vars-in-clauses clauses)))

;; Constructopr for contradcitions
(define (contradiction)
  'contradiction)

;; Accessor functions

;; Get the current binding
(define (binding f)
  (second f))

;; Get the current clause list
(define (clauses f)
  (first f))

;; Get the variable list
(define (vars f)
  (third f))


;; A binding is a (hash symbol? boolean?)

;; Constructor
(define (empty-binding)
  (hash))

;; Given an in-progress formula, bind x -> v
(define (bind f x v)
  (define new-binding (hash-set (binding f) x v))
  (formula (clauses f) new-binding (vars f)))


;; Functions for manipulating literals and atoms


;; A literal is one of:
;; atom
;; (list '- atom)

;; Extract the atom from a literal
(define (literal->atom literal)
  (if (negative-literal? literal)
      (second literal)
      literal))

;; Is the literal a negation?
(define (negative-literal? literal)
  (and (list? literal)
       (eq? (first literal) '-)))


(define (positive-literal? literal)
  (not (negative-literal? literal)))

;; Extract the variable a literal contains (raises an exception if the literal is not a variable)
(define (literal->var literal)
  (atom->var (literal->atom literal)))

;; Extract the variable an atom contains (raises an exception if the literal is not a variable)
(define (atom->var atom)
  (match atom
    [(or 'true 'false) (raise (not-a-variable))]
    [_ atom]))

;; Extracts the "consequence" of a literal.
;; This is the value that the variable of a literal must be set to in order for the literal to evaluate to true
(define (literal->consequence literal)
  (cond
    [(negative-literal? literal) #f]
    [(positive-literal? literal) #t]))
   
;; Computes the set of all variables in a formula
(define (vars-in-clauses clauses)
  (apply set-union (map vars-in-clause clauses)))

;; Computes the set of all variables in a clause
(define (vars-in-clause clause)
  (apply set-union (map var-in-literal clause)))

;; Computes the set of all variables in a literal (either the empty set or a singleton set)
(define (var-in-literal literal)
  (if (variable? literal)
      (list (literal->var literal))
      '()))

;; Is there a variable in this literal? or is `true` or `false`
(define (variable? literal)
  (match (literal->atom literal)
    [(or 'true 'false) #f]
    [_ #t]))

;; Exceptions

;; A contradiction exception is a 'contradiction

;; constructor
(define (contradiction-exception)
  'contradiction)

;; predicate
(define (contradiction-exception? x)
  (eq? x 'contradiction))


;; A unit exception is a (list 'unit-exception literal
;; constructor
(define (unit-exception literal)
  (list 'unit-exception literal))

;; predicate
(define (unit-exception? x)
  (and (list? x)
       (eq? (first x) 'unit-exception)))

;; Accessor
(define (unit-exception-literal unit-exception)
  (second unit-exception))

;; A not-a-variable excpetion is a 'not-a-variable

;; Constructor
(define (not-a-variable)
  'not-a-variable)

;; Utility functions

;; Returns a function that takes a single value and always returns `x`
(define (constant x)
  (λ (y) x))