RankTestExact

formal source

  59Optional algorithmic interface: a rank/null-space test can be plugged in as a
  60single Boolean oracle. This is intentionally abstract at scaffold stage.
  61-/
  62def RankTestExact {n N : ℕ} {φ : CNF n}
  63    (M : BWD3Model (n := n) (N := N) φ) : Prop :=
  64  ∃ decideLinear : Bool, decideLinear = true ↔ LinearFeasible M
  65
  66/--
  67Classical existence of an exact linear-feasibility decider.
  68
  69This theorem is purely logical (`decide` over a proposition) and does not provide
  70any complexity guarantee.
  71-/
  72theorem rankTestExact_classical {n N : ℕ} {φ : CNF n}
  73    (M : BWD3Model (n := n) (N := N) φ) : RankTestExact M := by
  74  classical
  75  refine ⟨decide (LinearFeasible M), ?_⟩
  76  simpa using (decide_eq_true_iff (p := LinearFeasible M))
  77
  78/--
  79If an exact linear-feasibility test is available, it immediately yields an
  80exact SAT decision predicate for the same instance.
  81-/
  82theorem sat_decider_from_rank_test {n N : ℕ} {φ : CNF n}
  83    (M : BWD3Model (n := n) (N := N) φ) (hRank : RankTestExact M) :
  84    ∃ decideSAT : Bool, decideSAT = true ↔ Satisfiable φ := by
  85  rcases hRank with ⟨d, hd⟩
  86  refine ⟨d, ?_⟩
  87  constructor
  88  · intro hdtrue
  89    have hlin : LinearFeasible M := (hd.mp hdtrue)
  90    exact (satisfiable_iff_linearFeasible M).2 hlin
  91  · intro hsat
  92    have hlin : LinearFeasible M := (satisfiable_iff_linearFeasible M).1 hsat