; Test cases, horribly formatted... (defvar *satisfiable1.cnf* '((A B )( (not D) ))) (defvar *satisfiable2.cnf* '((A Z (not Q) )( (not Z) )( A B Q )(M (not A) )( M (not Z) )( A (not M)))) (defvar *solveable.cnf* '(((not A) U (not Y) )((not Y) (not R) (not M) )(V (not D) X )(P (not O) M )(E I (not D) )((not J) (not G) (not H) )(Z (not C) L )((not U) (not O) Q )((not Q) (not A) R )(W (not D) H )((not B) X P )((not S) (not Q) W )((not Y) K Z )(A (not C) E )(G Y (not L) )((not O) (not F) M )(M (not Q) (not L) )((not E) (not S) I )(O (not Z) (not Z) )(V (not W) B )(U (not Q) (not B) )(B E (not I) )(V (not D) (not B) )((not I) (not G) A )(U (not P) (not X) )((not F) (not Q) (not W) )(N L G )(I (not J) E )((not M) D R )(Q B G )(L L (not R) )(U C (not W) )(J O (not D) )(X E L )(G R (not V) )((not L) F (not P) )((not U) (not G) E )((not I) K M )((not L) S (not A) )(T V (not D) )((not I) (not H) (not C) )((not M) (not Q) P )(R (not P) M )((not P) (not T) (not I) )(J (not Z) (not D) )((not D) (not Q) V )((not M) Z F )((not X) A C )(W (not E) (not Y) )(S W R )(G A (not E) )((not C) E Q )(B (not W) (not E) )((not M) (not J) G )(M E M )((not C) J (not X) )(U W M )(K (not D) M )(Z Y P )((not U) (not N) U )((not X) W (not R) )((not F) (not R) (not N) )(M (not R) S )(M (not W) (not H) )(F (not H) M )((not B) B (not V) )(S (not X) (not C) )((not B) M (not K) )((not S) P (not P) )(T (not L) L )(J (not R) (not C) )(Y (not X) (not J) )((not P) O (not A) )(Y (not Y) (not D) )(Q P (not U) )((not A) F V )((not H) (not U) E )((not D) K (not S) )(X (not K) (not A) )((not D) D (not L) )(D (not J) U )(N N (not W) )((not A) (not J) E )(R G (not A) )((not F) (not K) A )((not J) Z O )(L E (not V) )(N V (not Y) )(R G (not M) )((not D) T W )(L (not O) (not A) )(K J N )((not F) (not Z) D )(P (not E) (not E) )(S (not Y) F )((not K) (not D) (not E) )(X G (not A) )(V U T )(R M (not R) )((not T) C (not B) )((not I) P U )((not K) E (not H) )(U (not D) A )((not W) G P )(R S Z )((not S) (not V) (not B) )((not N) (not S) T )(B (not X) A )((not N) A V )(B A H )((not P) U T )(S (not X) P )(E (not D) S )(N Q J )(G (not D) B )(R (not R) P )(V O (not A) )((not E) S (not D) )((not Z) (not A) (not T) )(Y (not Z) (not S) )((not A) K (not T) )((not L) J P )(U M C )((not V) S Z )(L (not E) (not X) )(X (not V) (not M) )(H (not R) (not Y) )((not V) T (not R) )((not Y) X Z )(I (not F) R))) (defvar *test1.cnf* '((A F )( R )( F (not G) A )( F )( (not R) (not F) A )( D F (not D) G))) (defvar *test2.cnf* '((A F )( R )( F (not G) A )( F )( (not R) (not F) A )( D F (not D) G )( F )( (not R) (not F) A )( D A )( F (not G) A (not F) )( (not R) (not F) F (not G) A )( F )( (not R) (not F) (not G) A )( F )( (not F) (not G) ))) (defvar *test3.cnf* '(((not A) R Q )((not S) G )((not U) (not K) (not T) )((not Q) D )((not A) V (not I) )(W L (not F) )(K (not T) (not C) )((not D) (not W) )((not B) (not V) Q )((not E) (not P) (not K) )((not R) C )(U R L )((not P) (not K) )((not W) R (not T) )(C (not Z) K )(C (not A) )(A (not I) U )(A F I )((not A) (not A) Z )((not E) U (not R) )(R (not E) (not A) )(W K G )(I (not G) )(Z A R )(Z A )(Z (not A) )((not A) (not R) )(A R )((not Z) A )((not F) )(P (not Q) )(J (not A) (not K) )(A P )(B K )((not Z) (not F) (not R) )((not B) (not R) J )(R L (not A) )(U C )(Z V )(J (not J) (not M) )(F (not A) W )((not T) (not D) )((not P) B )(V (not E) )(W T )((not W) F )((not A) (not X) J )((not K) Z X )(B (not Q) )((not P) K )(W )((not G) H X )((not C) (not X) (not T) )(H (not A) Q )( (not J) (not Q) )(T (not S) )((not L) (not W) F )((not K) R )((not S) U )(B (not E) (not I) )(H B D )((not D) (not G) )((not B)))) (defvar *test4.cnf* '(((not P) (not K) L )(C (not K) )(F (not K) (not B) )((not F) B (not D) )(N Z (not W) )(E J )((not U) X R )(E (not M) D )((not X) )((not Q) (not N) (not B) )(N M P )((not H) C V )(C A )(B F )(Y X D )((not K) I S )(L Q B )(E (not S) (not N) )((not B) W (not D) )(J (not R) (not F) )((not Y) R )(N M P )((not H) C )(C A )(B F )(Y X D )((not K) I S )((not X) )(L Q B )(Y X D )((not K) I S )(L Q B )(E (not S) (not N) )((not B) W (not D) )(J (not R) (not F) )((not Y) R )((not X) )((not H) N (not P) )(O F P )((not X) )((not K) (not J) N )(B N M )((not J) (not G) V )(U X (not O) )((not Z) G E )(Y X D )((not K) I S )(B )(E (not S) (not N) )(Z G (not N) )(Y X D )((not K) I S )(L Q B )(E (not S) (not N) )( (not X) )((not S) W (not Z) )((not E) (not X) Q )(T S X )(V P (not W) )((not D) T (not H) )((not P) L (not K) )((not E) (not Q) (not E) )(C J U )((not B) J X )((not K) (not O) (not W) )((not O) A Y )(J E (not Y) )(V (not C) S )((not C) W (not D) )((not S) T T )((not J) (not J) T )(V (not D) (not T) )(G N (not I) )(Q H (not M) )(R (not F) (not P) )(V L (not U) )((not R) N C )(M (not S) (not B) )(Z K W )((not M) (not T) (not L) )(I Q U )((not N) F X )(T (not F) (not R) )(H K V )((not D) P (not Q) )(U O (not I) )((not G) )(K B (not Q) )((not F) R (not N) )((not S) (not K) R )(B (not K) )(S (not F) (not Y) )((not S) (not K) R )(B (not K) )(S (not F) (not Y) )((not H) (not V) (not P) )((not Y) O (not V) )((not C) (not G) H )(L (not F) (not Z) )(L (not Y) (not S) )((not V) (not I) )(K R F )(D V (not T) )((not J) (not R) (not S) )(R (not Q) X )((not I) V )((not C) (not Y) (not H) )(E (not T) S )(V (not I) Z )((not D) J (not Y) )(M (not D) L )(M (not N) (not P) )((not G) (not D) (not Z) )(B Z C )(G (not O) (not L) )(O (not X) )((not F) Q S )(P G )((not H) A D )((not S) (not T) (not H) )((not C) J (not Y) )((not H) O L )((not X) W )((not Q) B (not I) )(F X (not I) )((not G) O (not R) )(J (not K) (not F) )((not W) P F )((not Z) (not F) O )(L (not G) (not I) )((not R) W (not T)))) (defvar *test5.cnf* '(((not F) (not M) (not D) )((not J) J (not H) )((not V) R (not H) )(O (not E) (not F) )((not C) J (not T) )((not F) (not F) Z )((not Q) (not M) H )(X F (not E) )((not Q) (not D) (not A) )((not O) (not O) J )(O (not F) (not U) )((not T) (not Y) (not B) )(W Q (not K) )((not G) (not J) N )(D Q L )((not N) M (not Q) )((not P) (not A) S )(J X (not K) )(Z Y Q )(L I F )((not W) (not I) I )(Z (not O) (not Z) )((not Y) U (not W) )(K I X )((not C) Y (not O) )(M O D )(E (not A) U )(E (not E) (not W) )(J C H )(D X (not T) )((not D) F K )((not J) I (not M) )(U (not U) Q )((not S) (not W) (not D) )((not B) Z (not Y) )((not F) G (not K) )(L T (not G) )(I S (not Y) )(B (not W) O )(F N I )((not I) D (not S) )((not X) Q Y )(A (not Z) (not Z) )(P R V )(Q (not I) (not N) )(Z B (not F) )((not A) O (not I) )(F (not W) X )((not F) (not W) (not C) )(O N (not C) )((not V) (not O) B )((not G) P M )(V (not Q) X )(N H (not X) )(W (not S) (not S) )((not Q) (not V) J )(N H (not H) )(P (not A) I )((not J) H (not R) )((not L) C K )(Q (not F) X )(N D (not F) )((not E) I (not R) )(C X Z )(C (not F) (not I) )(Y (not W) W )(T (not Q) B )(I O T )(N (not E) (not A) )(J K D )((not R) F M )(G F (not J) )((not V) R (not F) )(V (not W) H )(C A O )(B G (not V) )((not S) Z (not F) )((not L) O (not U) )(Y W (not L) )((not Y) H K )((not E) (not O) (not T) )((not C) B (not Z) )(V (not X) (not M) )((not V) J (not L) )(L (not F) (not C) )(F (not A) C )((not J) O (not F) )((not F) W N )(O S (not U) )(J S (not D) )((not P) A W )((not K) (not Z) (not O) )((not Q) N (not Q) )((not O) R (not P) )(R (not X) N )((not E) Q (not Z) )((not S) C L )((not G) E (not Y) )(S (not T) (not T) )((not T) A (not J) )((not A) (not J) Q )(E Y N )(I (not N) A )(D (not F) (not L) )(D (not K) E )(Y R (not V) )((not D) S (not E) )(Y U (not W) )((not W) Z J )(E O F )(W R H )(R D K )(Y V (not R) )(K G (not N) )((not B) (not I) (not Y) )(L L Q )(Q Z E )(R W (not R) )((not Y) (not L) (not K) )((not H) (not X) (not D) )((not S) C (not J) )((not T) H H )(E (not Q) B )(P (not H) (not B) )((not A) O I )((not U) (not G) O )((not A) G Q )(X A G )((not Q) (not Q) A )((not Z) L (not F)))) (defvar *unsatisfiable1.cnf* '((A )( (not A)))) (defvar *unsatisfiable2.cnf* '((Q (not W) )( (not Q) )( A B W )( (not P) )( P (not B) )( (not A) (not P) )( A Q )( (not A) )( P )( (not P) A))) (defun symbols-in-sentence (sentence) (remove-duplicates (mapcan (lambda (clause) (mapcar (lambda (x) (if (listp x) (second x) x)) clause)) sentence))) (defun no-clauses-p (sentence) (not sentence)) (defun has-empty-clause-p (sentence) (> (count nil sentence) 0)) (defun appears-in-clause (clause sym) (when clause (cond ((eql (car clause) sym) 'positive) ((and (listp (car clause)) (eql (caar clause) 'not) (eql (cadar clause) sym)) 'negative) (t (appears-in-clause (cdr clause) sym))))) (defun pure-symbols (sentence symbols) (remove nil (mapcar (lambda (sym) (let* ((appearances (remove nil (mapcar (lambda (clause) (appears-in-clause clause sym)) sentence))) (uniq-appear (remove-duplicates appearances))) (if (> (length uniq-appear) 1) nil (if (eql (car uniq-appear) 'negative) (cons sym nil) (cons sym t))))) symbols))) (defun unit-clause (sentence symbols) (when sentence (if (= 1 (length (car sentence))) (if (listp (caar sentence)) (cons (second (caar sentence)) nil) (cons (caar sentence) t)) (unit-clause (cdr sentence) symbols)))) (defun assign-and-reduce (sentence new-assignment) (labels ((assign-and-reduce-one (sentence sym val) (mapcan (lambda (clause) (let* ((appears (appears-in-clause clause sym)) (appears-val (eql appears 'positive))) (if (not appears) (list clause) (if (eql appears-val val) nil (list (remove-if (lambda (x) (if (listp x) (eql (second x) sym) (eql x sym))) clause)))))) sentence))) (if (not new-assignment) sentence (assign-and-reduce-one (assign-and-reduce sentence (cdr new-assignment)) (car (car new-assignment)) (cdr (car new-assignment)))))) (defun dpll (sentence symbols assignments) (format t "dpll ~{~a~^, ~}~%" (list sentence symbols assignments)) (labels ((dpll-recurse (new-assignment) (dpll (assign-and-reduce sentence new-assignment) (set-difference symbols (mapcar #'car new-assignment)) (append assignments new-assignment)))) (cond ((no-clauses-p sentence) (list t assignments)) ((has-empty-clause-p sentence) (list nil assignments)) (t (let ((pure (pure-symbols sentence symbols))) (if pure (dpll-recurse pure) (let ((unit (unit-clause sentence symbols))) (if unit (dpll-recurse (list unit)) (let ((res (dpll-recurse (list (cons (car symbols) t))))) (if (car res) res (dpll-recurse (list (cons (car symbols) nil))))))))))))) (defun satisfiable (sentence) (dpll sentence (symbols-in-sentence sentence) '())) (defun satisfies-clause (clause assignments) (some (lambda (sym) (if (consp sym) (not (cdr (assq (second sym) assignments))) (cdr (assq sym assignments)))) clause)) (defun satisfies (sentence assignments) (every (lambda (clause) (satisfies-clause clause assignments)) sentence)) (defun brute-force-sat (sentence symbols assignments) (if symbols (let ((cur (car symbols))) (or (brute-force-sat sentence (cdr symbols) (cons (cons cur t) assignments)) (brute-force-sat sentence (cdr symbols) (cons (cons cur nil) assignments)))) (if (satisfies sentence assignments) assignments nil))) (defun check-sanity (sentence) (let ((result (satisfiable sentence))) (if (car result) (satisfies sentence (second (satisfiable sentence))) (not (brute-force-sat sentence (symbols-in-sentence sentence) nil))))) (defun print-sat (sentence) (let ((result (satisfiable sentence))) (if (car result) (mapcar (lambda (assignment) (format t "~a = ~:[false~;true~]~%" (car assignment) (cdr assignment))) (sort (cadr result) (lambda (x y) (string< (symbol-name (car x)) (symbol-name (car y)))))) (format t "Unsatisfiable"))))