SAT2-LISP.rkt

#lang racket

(define sample-predicates '(
  ("~X" "Y")
  ("~Y" "Z")
  ("X" "~Z")
  ("Z" "Y")
))

; Quick initialization
(define (init pairs)
  (graph-init graph pairs))

; Instantiate graph
(define graph (make-hash))

; Set up adjacency list using hash table
(define (graph-init graph pairs)
  (define (make-or-set key value)
    (cond ((hash-has-key? graph key)
           (hash-set! graph key (cons value (hash-ref graph key))))
          (else
           (hash-set! graph key (cons value '()))))
    (cond ((hash-has-key? graph value) '())
          (else
           (hash-set! graph value '()))))
  (cond ((empty? pairs) '())
        (else
         (define pair (car pairs))
         (make-or-set (car pair) (car (cdr pair)))
         (graph-init graph (cdr pairs)))))

; More readable node indexing
(define (node graph x)
  (hash-ref graph x))

(define (dfs graph start)
  (define visited (make-hash))
  (define (dfs-r graph visited start)
    (cond ((hash-has-key? visited start) '())
          (else
           (hash-set! visited start #t)
           (cons start (cons (map (lambda (x) (dfs-r graph visited x)) (node graph start)) '())))))
  (dfs-r graph visited start))

(define (reachable? graph start finish)
  (define visited (make-hash))
  (define (dfs-r graph visited start)
    (if (eq? start finish) 
        #t
        (cond ((hash-has-key? visited start) #f)
               (else
                (hash-set! visited start #t)
                (or (map (lambda (x) (dfs-r graph visited x)) (node graph start)))))))
  (dfs-r graph visited start))       

; Generate edges from a given 'OR' predicate (e.g. ("X" "Y") means X u Y)
(define (generate-edges predicate)
  (define (make-not x) (string-append "~" x))
  (define neg-fst (eq? (string-ref (car predicate) 0) #\~))
  (define fst (if neg-fst (substring (car predicate) 1 2) (car predicate)))
  (define neg-snd (eq? (string-ref (cadr predicate) 0) #\~))
  (define snd (if neg-snd (substring (cadr predicate) 1 2) (cadr predicate)))
  (cond ((and (not neg-fst) (not neg-snd))
         (list (list (make-not snd) fst) (list (make-not fst) snd)))
        ((and neg-fst (not neg-snd))
         (list (list fst snd) (list (make-not snd) (make-not fst))))
        ((and (not neg-fst) neg-snd)
         (list (list snd fst) (list (make-not fst) (make-not snd))))
        ((and neg-fst neg-snd)
         (list (list fst (make-not snd)) (list snd (make-not fst))))))

(define (generate-all-edges xs)
  (cond ((empty? xs) '())
        (else
         (cons
          (generate-edges (car xs))
          (generate-all-edges (cdr xs))))))

(define (flatten-pairs pairs)
  (cond ((empty? pairs) '())
        (else
         (cons (caar pairs) (cons (cadar pairs) (flatten-pairs (cdr pairs)))))))

(define l (generate-all-edges '(
  ("~X" "Y")
  ("~Y" "Z")
  ("X" "~Z")
  ("Z" "Y")
)))

; Initialize solver
(define solver (make-hash))
(define (solver-generate predicates)
  (graph-init solver (flatten-pairs (generate-all-edges predicates))))

(define (solve-for variable)
  (dfs solver variable))