A SAT prover in 50 lines of Arc

Here is a very naïve implementation of a purely functional SAT prover written in Arc. Deals with unit clauses and can read CNF files.

(def rem-members (source lst) ; source - lst
   (rem [mem _ lst] source))

(def has-members (source lst) ; inter (source, lst) != nil
   (some [mem _ lst] source))

(def simplify (clauses (o model))
   (withs
      (anti-model    (map - model)
       not-t-clauses (keep [~has-members _ model] clauses)
       simpl         (map [rem-members _ anti-model] not-t-clauses))
      (if (some nil simpl) ; At least one empty clause : UNSAT
         'UNSAT
         (aif (keep [is (len _) 1] simpl) ; if there are unit clauses...
            (simplify (rem (car it) simpl) ; Remove the first one
                      (cons (caar it) model)) ; And unify its literal
            (cons simpl model)))))

(def free-var (model) ; Chooses a non-unified var.
   (with
      (_abs (map abs model)
       i 1)
      (while (mem i _abs) (++ i))
      i))

(def solve (clauses (o model))
   (let simpl (simplify clauses model)
      (if (is 'UNSAT simpl)
         'UNSAT
         (with
            (c (car simpl)
             m (cdr simpl))
            (if (no c) ; We have no more clause : SAT
               m
               (withs
                  (var       (free-var m)
                   unif-true (solve c (cons var m)))
                  (if (isnt unif-true 'UNSAT)
                     unif-true
                     (solve c (cons (- var) m)))))))))

(def read-pb (filename)
   (let clauses '()
      (w/infile f filename
         (readline f)  ; ignore first line
         (whilet line (readline f)
            (let lits (tokens line)
               (if (and lits (~mem "c" lits)) ; Ignore empty lines and comments
                  (push (rem 0 (map [coerce _ 'int] lits)) clauses)))))
      clauses))

Enjoy !