 (defn lt-seq
   "Constructs a constraint stating that at most `k` of the given variables `xs` are true.
 
-  This is from ??.
+  Input: A list `xs` of variables and a number `k`
+  Output: A CNF stating that at most k of the variables are true,
+  usable for rolling-stones sat solver.
 
-  Could be replaced by `rolling-stones.core/at-most`."      ; todo paper name
+  This is from \"Towards an optimal CNF Encoding of Boolean Cardinality
+  Constraints\", Carsten Sinz (2005).
+  Could be replaced by `rolling-stones.core/at-most`."
   ([xs k]
    (lt-seq xs k (Math/random)))
   ([xs k prefix]



(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]

  The coordinates are returned in the form `[[e1 [x1 y1]] [e2 [x2 y2]] ...]`
  where e is the element, and x and y are the corresponding coordinates.

  See Section 5.2, Dürrschnabel, Hanika, Stumme (2019) https://arxiv.org/abs/1903.00686"
  ([graph]
   (compute-coordinates (lg/nodes graph) #(lg/has-edge? graph %1 %2)))
  ([P <=]
