diff --git a/LeanSAT/BitBlast/BoolExpr/Basic.lean b/LeanSAT/BitBlast/BoolExpr/Basic.lean
index 164430e6..eb2097da 100644
--- a/LeanSAT/BitBlast/BoolExpr/Basic.lean
+++ b/LeanSAT/BitBlast/BoolExpr/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import LeanSAT.Sat.Basic
+import LeanSAT.Sat
 
 set_option linter.missingDocs false
 
diff --git a/LeanSAT/CNF/Basic.lean b/LeanSAT/CNF/Basic.lean
index 534a2a6e..b50de2e7 100644
--- a/LeanSAT/CNF/Basic.lean
+++ b/LeanSAT/CNF/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import LeanSAT.Sat
+import LeanSAT.CNF.Literal
 
 open Sat
 
diff --git a/LeanSAT/Sat/Literal.lean b/LeanSAT/CNF/Literal.lean
similarity index 96%
rename from LeanSAT/Sat/Literal.lean
rename to LeanSAT/CNF/Literal.lean
index 022c9686..c9a9610a 100644
--- a/LeanSAT/Sat/Literal.lean
+++ b/LeanSAT/CNF/Literal.lean
@@ -3,7 +3,7 @@ Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
-import LeanSAT.Sat.Basic
+import LeanSAT.Sat
 
 abbrev Literal (α : Type u) := α × Bool
 
diff --git a/LeanSAT/LRAT/Assignment.lean b/LeanSAT/LRAT/Assignment.lean
index de62ea8d..b802fd7b 100644
--- a/LeanSAT/LRAT/Assignment.lean
+++ b/LeanSAT/LRAT/Assignment.lean
@@ -3,9 +3,11 @@ Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
-import LeanSAT.Sat.Basic
+import LeanSAT.Sat
 import LeanSAT.Util.PosFin
 
+open Sat
+
 /-- The `Assignment` inductive datatype is used in the `assignments` field of default formulas (defined in
     Formula.Implementation.lean) to store and quickly access information about whether unit literals are
     contained in (or entailed by) a formula.
diff --git a/LeanSAT/LRAT/Clause.lean b/LeanSAT/LRAT/Clause.lean
index 05d72633..76d5c046 100644
--- a/LeanSAT/LRAT/Clause.lean
+++ b/LeanSAT/LRAT/Clause.lean
@@ -3,7 +3,6 @@ Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
-import LeanSAT.Sat.Basic
 import LeanSAT.CNF.Basic
 import LeanSAT.Util.PosFin
 import LeanSAT.Util.Misc
diff --git a/LeanSAT/LRAT/Formula/Class.lean b/LeanSAT/LRAT/Formula/Class.lean
index 79af559c..2114fe12 100644
--- a/LeanSAT/LRAT/Formula/Class.lean
+++ b/LeanSAT/LRAT/Formula/Class.lean
@@ -3,7 +3,7 @@ Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
-import LeanSAT.Sat.Basic
+import LeanSAT.Sat
 import LeanSAT.LRAT.Clause
 
 namespace LRAT
diff --git a/LeanSAT/LRAT/LRATChecker.lean b/LeanSAT/LRAT/LRATChecker.lean
index 7e51d47d..3e53a726 100644
--- a/LeanSAT/LRAT/LRATChecker.lean
+++ b/LeanSAT/LRAT/LRATChecker.lean
@@ -6,6 +6,8 @@ Authors: Josh Clune
 import LeanSAT.External.LRAT
 import LeanSAT.LRAT.Formula.Instance
 
+open Sat
+
 namespace LRAT
 
 inductive Result
diff --git a/LeanSAT/Sat.lean b/LeanSAT/Sat.lean
index 5541e855..f321b988 100644
--- a/LeanSAT/Sat.lean
+++ b/LeanSAT/Sat.lean
@@ -1,7 +1,123 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
+Authors: Josh Clune
 -/
-import LeanSAT.Sat.Basic
-import LeanSAT.Sat.Literal
+
+namespace Sat
+
+/--
+For variables of type `α` and clauses of type `β`, `HSat.eval p c` is meant to determine whether
+a clause `c` is true under assignment `p`.
+-/
+class HSat (α : Type u) (β : Type v) :=
+  (eval : (α → Bool) → β → Prop)
+
+
+scoped infix:25 " ⊨ " => HSat.eval
+scoped notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f)
+
+def unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop :=
+  ∀ (p : α → Bool), p ⊭ f
+
+/-- `f1` and `f2` are logically equivalent -/
+def liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2)
+    : Prop :=
+  ∀ (p : α → Bool), p ⊨ f1 ↔ p ⊨ f2
+
+/-- `f1` logically implies `f2` -/
+def limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2)
+    : Prop :=
+  ∀ (p : α → Bool), p ⊨ f1 → p ⊨ f2
+
+/-- `f1` is unsat iff `f2` is unsat -/
+def equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2)
+    : Prop :=
+  unsatisfiable α f1 ↔ unsatisfiable α f2
+
+def incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1)
+    (f2 : σ2) : Prop :=
+  ∀ (p : α → Bool), (p ⊭ f1) ∨ (p ⊭ f2)
+
+protected theorem liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : liff α f f :=
+  (fun _ => Iff.rfl)
+
+protected theorem liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2]
+    (f1 : σ1) (f2 : σ2)
+    : liff α f1 f2 → liff α f2 f1 := by
+  intros h p
+  rw [h p]
+
+protected theorem liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1]
+    [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3)
+    : liff α f1 f2 → liff α f2 f3 → liff α f1 f3 := by
+  intros f1_eq_f2 f2_eq_f3 p
+  rw [f1_eq_f2 p, f2_eq_f3 p]
+
+protected theorem limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : limplies α f f :=
+  (fun _ => id)
+
+protected theorem limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1]
+    [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3)
+    : limplies α f1 f2 → limplies α f2 f3 → limplies α f1 f3 := by
+  intros f1_implies_f2 f2_implies_f3 p p_entails_f1
+  exact f2_implies_f3 p $ f1_implies_f2 p p_entails_f1
+
+theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1]
+    [HSat α σ2] (f1 : σ1) (f2 : σ2)
+    : liff α f1 f2 ↔ limplies α f1 f2 ∧ limplies α f2 f1 := by
+  constructor
+  . intro h
+    constructor
+    . intro p
+      rw [h p]
+      exact id
+    . intro p
+      rw [h p]
+      exact id
+  . intros h p
+    constructor
+    . exact h.1 p
+    . exact h.2 p
+
+theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1)
+    (f2 : σ2) (h : liff α f1 f2)
+    : unsatisfiable α f1 ↔ unsatisfiable α f2 := by
+  constructor
+  . intros f1_unsat p p_entails_f2
+    rw [← h p] at p_entails_f2
+    exact f1_unsat p p_entails_f2
+  . intros f2_unsat p p_entails_f1
+    rw [h p] at p_entails_f1
+    exact f2_unsat p p_entails_f1
+
+theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1)
+    (f2 : σ2) (h : limplies α f2 f1)
+    : unsatisfiable α f1 → unsatisfiable α f2 := by
+  intros f1_unsat p p_entails_f2
+  exact f1_unsat p $ h p p_entails_f2
+
+theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2]
+    (f1 : σ1) (f2 : σ2)
+    : unsatisfiable α f1 → incompatible α f1 f2 := by
+  intro h p
+  exact Or.inl $ h p
+
+theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1]
+    [HSat α σ2] (f1 : σ1) (f2 : σ2)
+    : limplies α f1 f2 → incompatible α f1 f2 → unsatisfiable α f1 := by
+  intro h1 h2 p pf1
+  cases h2 p
+  . next h2 =>
+    exact h2 pf1
+  . next h2 =>
+    exact h2 $ h1 p pf1
+
+protected theorem incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2]
+    (f1 : σ1) (f2 : σ2)
+    : incompatible α f1 f2 ↔ incompatible α f2 f1 := by
+  constructor
+  . intro h p
+    exact Or.symm $ h p
+  . intro h p
+    exact Or.symm $ h p
diff --git a/LeanSAT/Sat/Basic.lean b/LeanSAT/Sat/Basic.lean
deleted file mode 100644
index 7b5df3c4..00000000
--- a/LeanSAT/Sat/Basic.lean
+++ /dev/null
@@ -1,122 +0,0 @@
-/-
-Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Josh Clune
--/
-
-/--
-For variables of type `α` and clauses of type `β`, `HSat.eval p c` is meant to determine whether
-a clause `c` is true under assignment `p`.
--/
-class HSat (α : Type u) (β : Type v) :=
-  (eval : (α → Bool) → β → Prop)
-
-namespace Sat
-
-scoped infix:25 " ⊨ " => HSat.eval
-scoped notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f)
-
-def unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop :=
-  ∀ (p : α → Bool), p ⊭ f
-
-/-- `f1` and `f2` are logically equivalent -/
-def liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2)
-    : Prop :=
-  ∀ (p : α → Bool), p ⊨ f1 ↔ p ⊨ f2
-
-/-- `f1` logically implies `f2` -/
-def limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2)
-    : Prop :=
-  ∀ (p : α → Bool), p ⊨ f1 → p ⊨ f2
-
-/-- `f1` is unsat iff `f2` is unsat -/
-def equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2)
-    : Prop :=
-  unsatisfiable α f1 ↔ unsatisfiable α f2
-
-def incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1)
-    (f2 : σ2) : Prop :=
-  ∀ (p : α → Bool), (p ⊭ f1) ∨ (p ⊭ f2)
-
-protected theorem liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : liff α f f :=
-  (fun _ => Iff.rfl)
-
-protected theorem liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2]
-    (f1 : σ1) (f2 : σ2)
-    : liff α f1 f2 → liff α f2 f1 := by
-  intros h p
-  rw [h p]
-
-protected theorem liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1]
-    [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3)
-    : liff α f1 f2 → liff α f2 f3 → liff α f1 f3 := by
-  intros f1_eq_f2 f2_eq_f3 p
-  rw [f1_eq_f2 p, f2_eq_f3 p]
-
-protected theorem limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : limplies α f f :=
-  (fun _ => id)
-
-protected theorem limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1]
-    [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3)
-    : limplies α f1 f2 → limplies α f2 f3 → limplies α f1 f3 := by
-  intros f1_implies_f2 f2_implies_f3 p p_entails_f1
-  exact f2_implies_f3 p $ f1_implies_f2 p p_entails_f1
-
-theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1]
-    [HSat α σ2] (f1 : σ1) (f2 : σ2)
-    : liff α f1 f2 ↔ limplies α f1 f2 ∧ limplies α f2 f1 := by
-  constructor
-  . intro h
-    constructor
-    . intro p
-      rw [h p]
-      exact id
-    . intro p
-      rw [h p]
-      exact id
-  . intros h p
-    constructor
-    . exact h.1 p
-    . exact h.2 p
-
-theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1)
-    (f2 : σ2) (h : liff α f1 f2)
-    : unsatisfiable α f1 ↔ unsatisfiable α f2 := by
-  constructor
-  . intros f1_unsat p p_entails_f2
-    rw [← h p] at p_entails_f2
-    exact f1_unsat p p_entails_f2
-  . intros f2_unsat p p_entails_f1
-    rw [h p] at p_entails_f1
-    exact f2_unsat p p_entails_f1
-
-theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1)
-    (f2 : σ2) (h : limplies α f2 f1)
-    : unsatisfiable α f1 → unsatisfiable α f2 := by
-  intros f1_unsat p p_entails_f2
-  exact f1_unsat p $ h p p_entails_f2
-
-theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2]
-    (f1 : σ1) (f2 : σ2)
-    : unsatisfiable α f1 → incompatible α f1 f2 := by
-  intro h p
-  exact Or.inl $ h p
-
-theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1]
-    [HSat α σ2] (f1 : σ1) (f2 : σ2)
-    : limplies α f1 f2 → incompatible α f1 f2 → unsatisfiable α f1 := by
-  intro h1 h2 p pf1
-  cases h2 p
-  . next h2 =>
-    exact h2 pf1
-  . next h2 =>
-    exact h2 $ h1 p pf1
-
-protected theorem incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2]
-    (f1 : σ1) (f2 : σ2)
-    : incompatible α f1 f2 ↔ incompatible α f2 f1 := by
-  constructor
-  . intro h p
-    exact Or.symm $ h p
-  . intro h p
-    exact Or.symm $ h p