#lang karp/reduction

(require "3sat.rkt"
         "iset.rkt"
         karp/lib/cnf
         karp/lib/graph
         karp/lib/graph-inspector
         karp/lib/mapping-reduction)

(define-forward-instance-construction
  #:from 3sat #:to iset
  (3sat->iset-v1 a-3sat-inst)

  (define Cs (clauses-of (ϕ a-3sat-inst)))
  (define V (for/set {(el l i) for [l ∈ (literals-of C)]
                               for [(C #:index i) ∈ (clauses-of (ϕ a-3sat-inst))]}))
  (define E1 (for/set {((el l1 i) . -e- . (el l2 j))
              for [l1 ∈ (literals-of C1)] for [l2 ∈ (literals-of C2)]
              for [(C1 #:index i) ∈ Cs] for [(C2 #:index j) ∈ Cs]
              if (literal-neg-of? l1 l2)}))
  (define E2 (for/set {((el (fst p) i) . -e- . (el (snd p) i))
              for [p ∈ (all-pairs-in (literals-of C))]
              for [(C #:index i) ∈ Cs]}))


  ; incorrect
  (create-iset-instance ([G (create-graph V (set-∪ E1 #;E2))]
                         [k (set-size Cs)])))

(define-forward-certificate-construction
  #:from 3sat #:to iset
  (3sat->iset->>-cert-v1 f->t-constr a-3sat-inst c^3sat)

  (for/set {(el
             (find-one [l ∈ C] s.t. (or (and (positive-literal? l)
                                             (lookup c^3sat (underlying-var l)))
                                        (and (negative-literal? l)
                                             (not (lookup c^3sat (underlying-var l))))))
             i)
             for [(C #:index i) in (ϕ a-3sat-inst)]})
  )

(define-backward-certificate-construction
  #:from 3sat #:to iset 
  (3sat->iset-<<-cert-v1 f->t-constr a-3sat-inst c^iset)

  (define X (vars-of (ϕ a-3sat-inst)))
  (define X-True
    (for/set {x for [x ∈ X]
                if (∃ [v in c^iset]
                      (and
                       (positive-literal? (_1s v))
                       (equal? (underlying-var (_1s v)) x)))}))
  (mapping
   [x ∈ X-True] ~> #t
   [x ∈ (set-minus X X-True)] ~> #f))




(define/3sat-instance foo ([ϕ (cnf ('x1 ∨ 'x2 ∨ 'x3)
                                   ((¬'x1) ∨ (¬'x2) ∨ 'x4))]))
(3sat->iset-v1 foo)

(check-reduction #:from 3sat #:to iset
                 3sat->iset-v1 3sat->iset->>-cert-v1 3sat->iset-<<-cert-v1)

(visualize (G (3sat->iset-v1 (get-counterexample))))