feat: cake_lpr interface

.gitattributes

@@ -0,0 +1 @@
+*.icnf filter=lfs diff=lfs merge=lfs -text

Examples/ApproxMC.lean

@@ -9,8 +9,6 @@ import Trestle
 
 open Trestle
 
-namespace Examples.ApproxMC
-
 instance : Solver IO := Solver.Impl.DimacsCommand "cadical"
 instance : Solver.ModelCount IO := Solver.Impl.ApproxMCCommand
 

Examples/CakeLPR.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 The Trestle Contributors.
+Released under the Apache License v2.0; see LICENSE for full text.
+
+Authors: James Gallicchio
+-/
+
+import Trestle
+
+open Trestle
+
+instance : Solver IO := Solver.Impl.CakeLpr
+  (solverCmd := "cadical")
+  (solverFlags := #["--lrat=true", "--no-binary"])
+  (cakelprCmd := "cake_lpr")
+
+def main : IO Unit := do
+  let x : IVar := 1
+  let y : IVar := 2
+  let z : IVar := 3
+  let formula : ICnf :=
+    #[ #[x, y, z], #[ -x ], #[ -y ], #[ -z ] ]
+  let res ← Solver.solve formula
+  IO.println res

Experiments/Keller/Autos.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2024 The Trestle Contributors.
+Released under the Apache License v2.0; see LICENSE for full text.
+
+Authors: James Gallicchio
+-/
+
+import Experiments.Keller.KellerGraph
+
+namespace Keller
+
+def KAuto (n s) := SimpleGraph.Iso (KGraph n s) (KGraph n s)
+
+def KClique.map (a : KAuto n s) (k : KClique n s) : KClique n s :=
+  ⟨(k.val.map a.toEmbedding.toEmbedding), by
+  have ⟨vs,{card_eq, isClique}⟩ := k
+  simp only [KClique, SimpleGraph.isNClique_iff,
+    Finset.card_map, card_eq, and_true]
+  clear card_eq
+  generalize hvs' : vs.map _ = vs'
+  simp [Finset.ext_iff] at hvs'
+  intro v₁ hv₁ v₂ hv₂ hne
+  simp [← hvs'] at hv₁ hv₂; clear hvs'
+  rcases hv₁ with ⟨v₁,hv₁,rfl⟩; rcases hv₂ with ⟨v₂,hv₂,rfl⟩
+  apply a.map_adj_iff.mpr
+  simp [SimpleGraph.isClique_iff]
+  replace hne : v₁ ≠ v₂ := fun h => hne (congrArg a.toFun h)
+  apply isClique ?_ ?_ hne <;> simp [hv₁, hv₂]
+  ⟩
+
+
+namespace KVertex
+
+def flip (mask : BitVec n) (v : KVertex n s) : KVertex n s :=
+  { bv := v.bv ^^^ mask, colors := v.colors }
+
+theorem bv_flip (mask) {v : KVertex n s} : (flip mask v).bv = v.bv ^^^ mask := rfl
+@[simp] theorem bv_colors (mask) {v : KVertex n s} : (flip mask v).colors = v.colors := rfl
+
+@[simp] theorem flip_flip (mask : BitVec n) {v : KVertex n s} : (v.flip mask).flip mask = v := by
+  simp [flip, BitVec.xor_assoc]
+
+
+def permute (f : Fin n → Fin s → Fin s) (v : KVertex n s) : KVertex n s :=
+  { bv := v.bv, colors := Vector.ofFn (fun j => (f j) v.colors[j]) }
+
+@[simp] theorem bv_permute (f) {v : KVertex n s} : (permute f v).bv = v.bv := rfl
+
+theorem colors_permute (f) (v : KVertex n s) {j h} :
+    (permute f v).colors[j]'h = (f ⟨j,h⟩) v.colors[j] := by
+  simp [permute]
+
+
+theorem permute_permute (f₁ f₂ : Fin n → Fin s → Fin s) {v} :
+    permute f₁ (permute f₂ v) = permute (fun j => f₁ j ∘ f₂ j) v := by
+  simp [permute]
+
+@[simp] theorem permute_id {v : KVertex n s} : permute (fun _ => id) v = v := by
+  simp [permute]
+  congr
+  ext i hi
+  simp
+
+
+def reorder (f : Fin n → Fin n) (v : KVertex n s) : KVertex n s :=
+  ⟨ BitVec.ofFn (v.bv[f ·])
+  , Vector.ofFn (v.colors[f ·])⟩
+
+theorem bv_reorder (f : Fin n → Fin n) (v : KVertex n s) {j hj} :
+    (v.reorder f).bv[j]'hj = v.bv[f ⟨j,hj⟩] := by
+  simp [reorder]
+
+theorem colors_reorder (f : Fin n → Fin n) (v : KVertex n s) {j hj} :
+    (v.reorder f).colors[j]'hj = v.colors[f ⟨j,hj⟩] := by
+  simp [reorder]
+
+theorem reorder_comp (f₁ f₂ : Fin n → Fin n) (v : KVertex n s)
+    : reorder f₁ (reorder f₂ v) = reorder (f₂ ∘ f₁) v := by
+  simp [reorder]
+
+@[simp] theorem reorder_id (v : KVertex n s) : reorder id v = v := by
+  ext <;> simp [reorder]
+
+end KVertex
+
+
+namespace KAuto
+
+def id : KAuto n s := RelIso.refl _
+
+def flip (mask : BitVec n) : KAuto n s :=
+  RelIso.mk ({
+    toFun := KVertex.flip mask
+    invFun := KVertex.flip mask
+    left_inv  := by intro; simp
+    right_inv := by intro; simp
+  }) (by
+    simp [KAdj, KVertex.bv_flip]
+  )
+
+@[simp] theorem toFun_flip {x : KVertex _ _ } :
+  DFunLike.coe (F := KAdj ≃r KAdj) (α := KVertex n s) (β := fun _ => KVertex n s)
+    (flip (n := n) (s := s) mask) x = KVertex.flip mask x := rfl
+
+def permute (f : Fin n → Fin s ≃ Fin s) : KAuto n s :=
+  RelIso.mk ({
+    toFun := KVertex.permute (fun j => f j)
+    invFun := KVertex.permute (fun j => (f j).symm)
+    left_inv  := by intro; simp [KVertex.permute_permute]
+    right_inv := by intro; simp [KVertex.permute_permute]
+  }) (by
+    intro v₁ v₂
+    simp [KAdj, KVertex.colors_permute])
+
+@[simp] theorem toFun_permute {x : KVertex _ _ } :
+  DFunLike.coe (F := KAdj ≃r KAdj) (α := KVertex n s) (β := fun _ => KVertex n s)
+    (permute (n := n) (s := s) f) x = KVertex.permute (fun j => f j) x := rfl
+
+def reorder (f : Fin n ≃ Fin n) : KAuto n s :=
+  RelIso.mk {
+    toFun := KVertex.reorder f
+    invFun := KVertex.reorder f.invFun
+    left_inv := by intro; simp [KVertex.reorder_comp]
+    right_inv := by intro; simp [KVertex.reorder_comp]
+  } (by
+    intro a b
+    simp [KAdj, KVertex.reorder]
+    constructor
+    · rintro ⟨j₁,hbv₁,hc1,j₂,hne,h⟩
+      use f j₁, hbv₁, hc1, f j₂
+      rw [EmbeddingLike.apply_eq_iff_eq]
+      simp [hne, h]
+    · rintro ⟨j₁,hbv₁,hc1,j₂,hne,h⟩
+      use f.symm j₁; simp
+      use hbv₁, hc1, f.symm j₂
+      rw [EmbeddingLike.apply_eq_iff_eq]
+      simp [hne, h]
+  )
+
+@[simp] theorem toFun_reorder {x : KVertex _ _ } :
+  DFunLike.coe (F := KAdj ≃r KAdj) (α := KVertex n s) (β := fun _ => KVertex n s)
+    (reorder (n := n) (s := s) f) x = KVertex.reorder (fun j => f j) x := rfl
+

Experiments/Keller/ConjectureResults.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 The Trestle Contributors.
+Released under the Apache License v2.0; see LICENSE for full text.
+
+Authors: James Gallicchio
+-/
+
+import Experiments.Keller.G8_Clique
+
+namespace Keller
+
+/-! ## Positive Results -/
+
+-- These are all currently waiting on an updated proof that
+-- it suffices to check G_{n,2^(n-1)} instead of all s.
+
+axiom conjectureIn_iff_no_cliques (n) : conjectureIn n ↔ IsEmpty (KClique n (2^(n-1)))
+
+theorem conjectureIn_2 : conjectureIn 2 := by
+  rw [conjectureIn_iff_no_cliques, ← KCliqueData.checkAll_iff_isempty_kclique]
+  native_decide
+#print axioms conjectureIn_2
+
+theorem conjectureIn_3 : conjectureIn 3 := sorry
+theorem conjectureIn_4 : conjectureIn 4 := sorry
+theorem conjectureIn_5 : conjectureIn 5 := sorry
+theorem conjectureIn_6 : conjectureIn 6 := sorry
+theorem conjectureIn_7 : conjectureIn 6 := sorry
+
+theorem not_conjectureIn_8 : ¬ conjectureIn 8 := by
+  apply G8_clique.check_implies_not_conjecture
+  native_decide
+
+-- TODO(JG): finish this proof
+theorem not_conjectureIn_ge_8 : n ≥ 8 → ¬ conjectureIn 8 := by
+  sorry

Experiments/Keller/Encoding.lean

@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2024 The Trestle Contributors.
+Released under the Apache License v2.0; see LICENSE for full text.
+
+Authors: James Gallicchio
+-/
+
+import Trestle.Encode
+import Trestle.Solver.Dimacs
+import Trestle.Upstream.IndexTypeInstances
+import Experiments.Keller.KellerGraph
+import Experiments.Keller.SymmBreakSR
+
+namespace Keller.Encoding
+
+open Trestle Encode
+
+inductive Vars (n s : Nat)
+-- coordinates of each of the 2^n clique nodes
+| x (i : BitVec n) (j : Fin n) (k : Fin s)
+deriving IndexType, Hashable
+
+def allBitVecs (n) : Array (BitVec n) := Array.ofFn (BitVec.ofFin)
+
+section Base
+open EncCNF Model PropForm
+
+-- ensure that each vertex has a defined coordinate on each dimension
+def coordinates : EncCNF (Vars n s) Unit := do
+  for i in allBitVecs n do
+    for j in Array.finRange n do
+      let vars := Array.ofFn (fun k => Literal.pos <| Vars.x i j k)
+      -- at least one of the `c_ij-` variables is true
+      addClause vars
+      -- at most one of the `c_ij-` variables is true
+      Cardinality.amoPairwise vars
+
+-- ensure for all pairs where only one coordinate *must* be different,
+-- that there is a second coordinate which is also different
+def twoDiffs : EncCNF (Vars n s) Unit := do
+  for i in allBitVecs n do
+    for j in Array.finRange n do
+      -- the bitvector which must be different only at coord `j`
+      let i' : BitVec n := i ||| BitVec.shiftLeft 1 j
+      -- when `j` bit is already high, `i = i'`, so filter that out
+      if i < i' then
+        withTemps (Fin n × Fin s) (do
+          for j' in List.finRange n do
+            if j' ≠ j then
+              for k in List.finRange s do
+                let temp := Literal.neg (Sum.inr (j',k))
+                addClause #[temp, Literal.pos <| Sum.inl (Vars.x i j' k), Literal.pos <| Sum.inl (Vars.x i' j' k)]
+                addClause #[temp, Literal.neg <| Sum.inl (Vars.x i j' k), Literal.neg <| Sum.inl (Vars.x i' j' k)]
+          addClause (Array.mk (do
+            let j' ← List.finRange n
+            guard (j' ≠ j)
+            let k ← List.finRange s
+            return Literal.pos (Sum.inr (j',k))
+          ))
+        )
+
+-- true if `i` and `i'` on coord `j` are equal `mod s`
+def hasSGapAt (i i' : BitVec n) (j : Fin n) : PropForm (Vars n s) :=
+  all (do
+    let k ← List.finRange s
+    return [propform| {Vars.x i j k} ↔ {Vars.x i' j k}]
+  )
+
+-- ensures `i` and `i'` have a coord `j` on which they are equal `mod s`
+def hasSGap (i i' : BitVec n) : EncCNF (Vars n s) Unit :=
+  -- only can consider those `j` for which `i` and `i'` could have an `s`-gap
+  let potentialJs := Array.finRange n |>.filter fun j => i[j] ≠ i'[j]
+  withTemps (Fin n) (do
+    for j in potentialJs do
+      for k in List.finRange s do
+        addClause #[Literal.neg (Sum.inr j), Literal.pos (Sum.inl (.x i j k)), Literal.neg (Sum.inl (.x i' j k))]
+        addClause #[Literal.neg (Sum.inr j), Literal.neg (Sum.inl (.x i j k)), Literal.pos (Sum.inl (.x i' j k))]
+    addClause (potentialJs |>.map (Literal.pos <| Sum.inr ·))
+  )
+
+def allSGap : EncCNF (Vars n s) Unit := do
+  for i in allBitVecs n do
+    for i' in allBitVecs n do
+      if i < i' then
+        hasSGap i i'
+
+def baseEncoding (n s) : EncCNF (Vars n s) Unit := do
+  coordinates
+  twoDiffs
+  allSGap
+
+end Base
+
+section SymmBreaking
+open EncCNF Vars
+
+def triangle (L : List α) (n : Nat) : List (Vector α n) :=
+  aux L n |>.map (·.reverse)
+where aux (L : List α) (n : Nat) : List (Vector α n) :=
+  match n with
+  | 0 => [⟨#[], by simp⟩]
+  | n+1 =>
+    L.tails.flatMap (fun
+      | []     => []
+      | hd::tl =>
+        aux (hd::tl) n |>.map (·.push hd)
+    )
+
+def canonicalColumn (start : Fin s) (len : Nat) : List (Vector (Fin s) len) :=
+  aux start len |>.map (Vector.reverse)
+where aux (start : Fin s) (len) : List (Vector (Fin s) len) :=
+  have : NeZero s := ⟨fun h => (h ▸ start).elim0⟩
+  match len with
+  | 0 => [⟨#[],by simp⟩]
+  | len+1 => do
+    let tail := aux start len
+    (List.range (start+1)).flatMap (fun hd =>
+      let hd : Fin s := hd
+      tail.map (·.push hd)) ++
+    (aux (start+1) len).map (fun tl =>
+      tl.push (Fin.ofNat' s (start+1)))
+
+def canonicalColumns (n : Nat) (len : Nat) (hs : s > 0) : List (Vector (Vector (Fin s) len) n) :=
+  let cols := canonicalColumn (s := s) ⟨0,hs⟩ len
+  triangle cols n
+
+
+def symmBreak (n s) : EncCNF (Vars n s) Unit := do
+  if hs : s ≥ 2 then do
+  if hn : n ≥ 2 then do
+  -- c0 = (0,0,0,0,0,0,0)
+  for hi : i in [0:n] do
+    have : i < n := hi.2
+    set 0 i 0
+  -- c1 = (s,1,0,0,0,0,0)
+  set 1 0 0
+  set 1 1 1
+  for hi : i in [2:n] do
+    have : i < n := hi.2
+    set 1 i 0
+  if hn' : n ≥ 5 then do
+    -- c3 = (s,s+1,1,1,1,*,*)
+    set 3 0 0
+    for hi : i in [1:5] do
+      have : i < 5 := hi.2
+      set 3 i 1
+where set (a b c) (hb : b < n := by omega) (hc : c < s := by omega) :=
+  unit <| .pos <| x a ⟨b,hb⟩ ⟨c,hc⟩
+
+def symmBreakCubes (hn : n ≥ 5) (hs : s ≥ 4) : List (Clause <| Literal (Vars n s)) :=
+  let matrixList := canonicalCases.toList
+  let colsList := canonicalColumns (n-5) 4 (by omega)
+  let idxs := #[3, 7, 11, 19]
+  matrixList.flatMap fun m =>
+    let matAssn := Array.mk <| List.flatten <|
+      List.ofFn fun r => List.ofFn fun c =>
+        let mval : Fin s := m.data[r][c].castLE (by omega)
+        .pos (x idxs[r.succ] ⟨2+c, by omega⟩ mval)
+    colsList.map fun cols =>
+      matAssn ++ Array.flatten (
+        Array.ofFn (n := 4) fun r => Array.ofFn (n := n-5) fun c =>
+          .pos <| x idxs[r] ⟨c+5, by omega⟩ cols[c][r])
+
+end SymmBreaking
+
+def fullEncoding (n s) : EncCNF (Vars n s) Unit := do
+  baseEncoding n s
+  symmBreak n s