;; SAT-solver.lisp - a simple Lisp interface to the zchaff SAT solver.
;; Originally by Todd Neller
;; Ported to Lisp by Dave Musicant

;; Copyright (C) 2005 Dave Musicant

;; This program is free software; you can redistribute it and/or
;; modify it under the terms of the GNU General Public License
;; as published by the Free Software Foundation; either version 2
;; of the License, or (at your option) any later version.

;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; Information about the GNU General Public License is available online at:
;;   http://www.gnu.org/licenses/
;; To receive a copy of the GNU General Public License, write to the Free
;; Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
;; 02111-1307, USA.

(defun test-kb(clauses)
  (let ((maxvar 0))
     (with-open-file (out "query.cnf" :direction :output)
         (dolist (clause clauses)
           (dolist (literal clause)
             (setf maxvar (max (abs literal) maxvar))))
         (format out "c This DIMACS format CNF file was generated by SAT-solver.lisp~%")
         (format out "c Do not edit.~%")
         (format out "p cnf ~a ~a~%" maxvar (length clauses))
         (dolist (clause clauses)
           (dolist (literal clause)
             (format out "~a " literal))
           (format out "0~%")))

     (let ((answer nil))
       (with-open-stream (result (ext:run-shell-command 
                                  "zchaff query.cnf" :output :stream))
         (setf answer
               (loop for line = (read-line result nil)
                     while line do
                     (if (search "RESULT:" line)
                         (if (search "UNSAT" line)
                             (return 'UNSAT)
                           (return 'SAT))))))
      
       (cond ((equal answer 'SAT) t)
             ((equal answer 'UNSAT) nil)
             (t (progn
                  (format t "Error: Unexpected file end in query.cnf.~%")
                  nil))))))


(defun test-literal (literal clauses)
  (let ((result 'unknown) (query-clauses (list (list literal))))
     (if (not (test-kb (append clauses query-clauses)))
         (setf result 'false))
       (progn
         (setf query-clauses (list (list (* -1 literal))))
         (if (not (test-kb (append clauses query-clauses)))
             (setf result 'true)))
    result))

(defun SAT-solver-tester ()
  (let ((clauses '((-1 -2) (2  1) (-2 -3) (3 2) (-3 -1) (-3  -2) (1 2 3))))
    (format t "Knowledge base is satisfiable: ~a~%" (test-kb clauses))
    (format t "Is Cal a truth-teller? ")
    (let ((result (test-literal 3 clauses)))
          (cond ((equal result 'false) (format t "No.~%"))
                ((equal result 'true) (format t "Yes.~%"))
                (t (format t "Unknown.~%"))))))