<commit_before>(ns conexp.layouts.dim-draw
  (:require [ubergraph.core :as uber]
            [loom.graph :as lg]
            [conexp.fca.lattices :as lat]
            [conexp.fca.graph :refer :all]
            [conexp.util.graph :refer :all]
            [conexp.layouts.base :as lay]
            [conexp.base :exclude [transitive-closure] :refer :all]
            [rolling-stones.core :as sat :refer :all]))

(defn lt-seq
  "Constructs a constraint stating that at most `k` of the given variables `xs` are true.

  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.

  This is from \"Towards an optimal CNF Encoding of Boolean Cardinality
  Constraints\", <NAME> (2005).
  Could be replaced by `rolling-stones.core/at-most`."
  ([xs k]
   (lt-seq xs k (Math/random)))
  ([xs k prefix]
   (assert (>= k 0))
   (if (and (> k 0) (not (empty? xs)))
     (let [n (count xs)
           s prefix]
       (concat
         [[(! (xs 0)) [:tmp s 0 0]]]
         (map #(vec [(! [:tmp s 0 %])])
              (vec (range 1 k)))
         (mapcat (fn [i] (concat [
                                  [(! (xs i)) [:tmp s i 0]]
                                  [(! [:tmp s (- i 1) 0]) [:tmp s i 0]]]
                                 (mapcat (fn [j] [
                                                  [(! (xs i)) (! [:tmp s (- i 1) (- j 1)]) [:tmp s i j]]
                                                  [(! [:tmp s (- i 1) j]) [:tmp s i j]]])
                                         (vec (range 1 k)))
                                 [[(! (xs i)) (! [:tmp s (- i 1) (- k 1)])]]))
                 (vec (range 1 (- n 1))))
         [[(! (xs (- n 1))) (! [:tmp s (- n 2) (- k 1)])]]))
     (vec (map #(vec [(! %)]) xs)))))


(defn is-compatible
  "Checks if two edges are compatible.

  For an ordering given as graph and two edges e1 and e2 this means that the
  transitive closure of the graph with both edges added does not contain a
  (non-trivial) cycle."
  [digraph e1 e2]
  (let [tc (transitive-closure
             (uber/add-directed-edges digraph e1 e2))]
    (forall [e (lg/edges tc)]
            (or (= (lg/src e) (lg/dest e))
                (not (lg/has-edge? tc (lg/dest e) (lg/src e)))))))

(defn tig
  "Returns the \"transitive incompatibility graph\" (tig) for a given ordering
  (given ad graph).

  See Section 3, Dürrschnabel, Hanika, Stumme (2019) https://arxiv.org/abs/1903.00686"
  [graph]
  (let [ccg (co-comparability (lg/nodes graph) #(lg/has-edge? graph %1 %2))
        tig-nodes (map edge->vec (lg/edges ccg))]
    (reduce
      (fn [g-outer e1]
        (reduce
          (fn [g-inner e2]
            (if (is-compatible graph e1 e2)
              g-inner
              (uber/add-undirected-edges g-inner [e1 e2])))
          g-outer
          tig-nodes))
      (lg/add-nodes* (uber/graph) tig-nodes)               ; empty graph
      tig-nodes)))


(defn sat-reduction
  "Reduces the problem of finding a maximum bipartite subgraph to satisfiability
  and solves it.
<commit_msg>DimDraw: Now using lemma for speedup<commit_after>(ns conexp.layouts.dim-draw
  (:require [ubergraph.core :as uber]
            [loom.graph :as lg]
            [conexp.fca.lattices :as lat]
            [conexp.fca.graph :refer :all]
            [conexp.util.graph :refer :all]
            [conexp.layouts.base :as lay]
            [conexp.base :exclude [transitive-closure] :refer :all]
            [rolling-stones.core :as sat :refer :all]))

(defn lt-seq
  "Constructs a constraint stating that at most `k` of the given variables `xs` are true.

  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.

  This is from \"Towards an optimal CNF Encoding of Boolean Cardinality
  Constraints\", <NAME> (2005).
  Could be replaced by `rolling-stones.core/at-most`."
  ([xs k]
   (lt-seq xs k (Math/random)))
  ([xs k prefix]
   (assert (>= k 0))
   (if (and (> k 0) (not (empty? xs)))
     (let [n (count xs)
           s prefix]
       (concat
         [[(! (xs 0)) [:tmp s 0 0]]]
         (map #(vec [(! [:tmp s 0 %])])
              (vec (range 1 k)))
         (mapcat (fn [i] (concat [
                                  [(! (xs i)) [:tmp s i 0]]
                                  [(! [:tmp s (- i 1) 0]) [:tmp s i 0]]]
                                 (mapcat (fn [j] [
                                                  [(! (xs i)) (! [:tmp s (- i 1) (- j 1)]) [:tmp s i j]]
                                                  [(! [:tmp s (- i 1) j]) [:tmp s i j]]])
                                         (vec (range 1 k)))
                                 [[(! (xs i)) (! [:tmp s (- i 1) (- k 1)])]]))
                 (vec (range 1 (- n 1))))
         [[(! (xs (- n 1))) (! [:tmp s (- n 2) (- k 1)])]]))
     (vec (map #(vec [(! %)]) xs)))))


(defn is-compatible
  "Checks if two edges are compatible.

  For an ordering given as graph and two edges e1 and e2 this means that the
  transitive closure of the graph with both edges added does not contain a
  (non-trivial) cycle."
  [digraph e1 e2]
   (not(and
       (lg/has-edge? digraph (lg/dest e2) (lg/src e1))
       (lg/has-edge? digraph (lg/dest e1) (lg/src e2)))))

(defn tig
  "Returns the \"transitive incompatibility graph\" (tig) for a given ordering
  (given ad graph).

  See Section 3, Dürrschnabel, <NAME> (2019) https://arxiv.org/abs/1903.00686"
  [graph]
  (let [ccg (co-comparability (lg/nodes graph) #(lg/has-edge? graph %1 %2))
        tig-nodes (map edge->vec (lg/edges ccg))]
    (reduce
      (fn [g-outer e1]
        (reduce
          (fn [g-inner e2]
            (if (is-compatible graph e1 e2)
              g-inner
              (uber/add-undirected-edges g-inner [e1 e2])))
          g-outer
          tig-nodes))
      (lg/add-nodes* (uber/graph) tig-nodes)               ; empty graph
      tig-nodes)))


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

{'fraction_non_alphanumeric': 0.1491486574983628, 'fraction_numerical': 0.018009168303863784, 'mean_word_length': 1.680561649846424, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 12, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 20, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4730206', 'n_tokens_mistral': 2132, 'n_tokens_neox': 1993, 'n_words': 702}