 
 (defn draw-ascii
   [coords]
-  (let [
-        x-step 2
+  (let [x-step 2
         size (count coords)
         spaces (.substring (replicate-str "   " (* size x-step)) (* size x-step))
         line-contents (map (fn [i] (filter

         clauses (concat node-clauses edge-clauses no-more-than-k-bad-edges-clauses)
         raw-solution (sat/solve-symbolic-cnf clauses)
         C (map first (filter #(and (sat/positive? %) (= (% 1) 3)) raw-solution))]
     (println node-clauses)
     (println edge-clauses)
     (println no-more-than-k-bad-edges-clauses)
     (println "solved:")
     (println raw-solution)
     (println C)
     C)))

(sat-reduction (uber/graph [:a :b] [:a :c] [:b :e] [:c :e] [:a :e]) 1)

  (println line))

(defn sat-reduction
  "Reduces the problem of finding a maximum bipartite subgraph to satisfiability.


  As described in Section 5.2 of Dominik's paper."          ; todo paper name
  ([g]
   (first (drop-while #(= % nil) (map #(sat-reduction g %) (range)))))
  ([g k]
