dpll.rkt

;; Traditional Abstract DPLL (no clause learning)
;; See this paper: https://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf
#lang racket

(define (clause? cl)
  (match cl
    [`(,(? integer? x) ...) #t]
    [_ #f]))


(define (classify-clause cl M)
  (match cl
    [`(,lits ...)
     ;; accumulate the number of positive and negative literals
     (define pn (foldl (match-lambda** [(lit `(,pos ,neg))
                                        (let ([v (hash-ref M (abs lit) 'unassigned)])
                                          (match v
                                            ['unassigned `(,pos ,neg)]
                                            [#t (if (< lit 0) `(,pos ,(add1 neg)) `(,(add1 pos) ,neg))]
                                            [#f (if (< lit 0) `(,(add1 pos) ,neg) `(,pos ,(add1 neg)))]))])
                       '(0 0)
                       lits))
     (match pn
       [`(,pos ,neg)
        (cond [(> pos 0) 'satisfied]
              [(= 1 (- (length lits) neg)) 'unit]
              [(= (length lits) neg) 'conflicting]
              [else 'unassigned])])]))
  
;; If there is a unit clause in the current assignment
;; then return that clause, otherwise return #f
(define (has-unit-clause? clauses M)
  (foldl
   (λ (cl acc)
     (if acc
         acc
         (equal? (classify-clause cl M) 'unit)))
   #f
   (set->list clauses)))

;; DPLL States
(define (state? st)
  (match st
    [`((,M-tr ,M) ∥ ,F)
     (and (and (list? M-tr) (andmap integer? M-tr)) ;; M-tr
          (and (hash? M)
               (andmap integer? (hash-keys M))
               (andmap boolean? (hash-values M)))    ;; M
          (and (list? F) (andmap clause? F)))]
    ['FailState #t]
    [_ #f]))

(define (find-first-clause clauses M such-that)
  (call/cc (λ (k)
             (map (λ (cl) (if (equal? (classify-clause cl M) such-that)
                              (k cl)
                              #f))
                  (set->list clauses)))))

(define (find-first-unassigned-lit clause M)
  (call/cc (λ (k) (map (λ (lit) (if (not (hash-has-key? M (abs lit)))
                                                        (k lit)
                                                        #f))
                       clause))))

(define (⇒ state)
  (match state
    ;; UnitPropagate
    [`((,M-tr ,M) ∥ ,clauses) 
     #:when (has-unit-clause? clauses M)
     (let* ([unit-clause
             ;; walks over clauses until we find one that is unit
             (find-first-clause clauses M 'unit)]
            ;; walks over all literals until it finds one that is unassigned
            [ulit (find-first-unassigned-lit unit-clause M)])
       `((,(cons ulit M-tr) ,(hash-set M (abs ulit) (if (< ulit 0) #f #t))) ∥ ,clauses))]
    [`((,M-tr ,M) ∥ ,clauses)
     #:when (> (count (λ (cl) (equal? 'unassigned (classify-clause cl M))) (set->list clauses)) 0)
     (let* ([unassigned-clause
             ;; walks over clauses until we find one that is unassigned
             (find-first-clause clauses M 'unassigned)]
            ;; walks over all literals until it finds one that is unassigned
            [dlit (find-first-unassigned-lit unassigned-clause M)])
       `((,(cons `(d ,dlit) M-tr) ,(hash-set M (abs dlit) (if (< dlit 0) #f #t))) ∥ ,clauses))]
    [`((,M-tr ,M) ∥ ,clauses)
     #:when
     (and (> (count (λ (cl) (equal? 'conflicting (classify-clause cl M))) (set->list clauses)) 0)
          ;; the trail contains no decision literals
          (andmap (λ (trail-entry) (match trail-entry [`(d ,_) #f] [_ #t])) M-tr))
     ;; Top-level conflict
     'FailState]
    [`((,M-tr ,M) ∥ ,clauses)
     #:when
     (and (> (count (λ (cl) (equal? 'conflicting (classify-clause cl M))) (set->list clauses)) 0)
          ;; the trail contains a decision literal
          (ormap (λ (trail-entry) (match trail-entry [`(d ,_) #t] [_ #f])) M-tr))
     ;; helper function: pop from the trail and unassign until a decision
     (define (h M-tr M)
       (match (first M-tr)
         ;; the topmost decision literal
         [`(d ,lit) `((,(cons (- lit) (rest M-tr)) ,M) ∥ ,clauses)]
         ;; a lit that was from unit propagation
         [lit (h (rest M-tr) (hash-remove M lit))]))
     (h M-tr M)]
    [_ `(SAT ,state)]))

;; Some examples

#;(⇒
 (⇒
  (⇒ `((() ,(hash)) ∥ ,(set '(-1) '(1 4) '(1 -4 3))))))

;; clauses is a list of clauses
(define (inj clauses)
  `((() ,(hash)) ∥ ,(list->set clauses)))

(⇒ (⇒ (inj '((1 2) (-1 -2)))))

;; generate a big set of clauses and then run the propagator
#;(let* ([N 500]
       [nums (range 1 N)]
       [lits (map (λ (x) (if (= 0 (random 0 2)) (- x) x)) nums)]
       [clauses (list->set (map (λ (len)
                                  ;; take the first n-1
                                  (let ([first-n (take lits (- len 1))]
                                        [l (list-ref lits (- len 1))])
                                    (append (map - first-n) (list l))))
                                (range 1 N)))])
  ;(pretty-print clauses)
  (pretty-print (first (first (foldl (λ (i st)
                                       ;(pretty-print st)
                                       (⇒ st))
                                     `((() ,(hash)) ∥ ,clauses)
                                     (range 499))))))


(define (run clauses)
  (define (h st)
    (match st
      ['FailState (pretty-print 'UNSAT)]
      [`(SAT ,st) (pretty-print `(SAT ,(first (first st))))]
      [_ (pretty-print st)
         (pretty-print '⇒)
         (h (⇒ st))]))
  (h (inj clauses)))

;(run '((1 2) (-1 2) (1 -2) (-1 -2)))
;(run '((1 2) (-1 3) (-2 -3) (-1 -3)))
(run '((1 2 3) (-1 2) (-2 3 4) (-3 -4 5) (1 -5) (-1 -3 -5) (2 4 -5) (-1 -2 -3 -4 -5)))