How to remove quantifiers for specific instances of a SAT?

Stream: new members

[Aatman Supkar]

I have a SAT which depends on some variables, and I want to encode it in a format such that the bv_decide tactic can handle it. As a dummy example,

def SAT_ex1 {n : Nat} (x : BitVec (n+1)) : Vector Prop n :=
  Vector.ofFn (fun i ↦ x.getLsbD (i.val + 1) || ¬ x.getLsbD (i.val))

Or it could be a \forall i : Fin n hypothesis.

Now, I want to be able to arrange for things so that given an n, I am able to synthesise an expression which can be handled by bv_decide. How do I do this?

The plan here is to reduce an instance of a certain problem to a SAT, and then close the goal by calling bv_decide.

[Henrik Böving]

For situations like this I would recommend trying to build a simp set that can get you there, for example:

import Std.Tactic.BVDecide

def SAT_ex1 {n : Nat} (x : BitVec (n+1)) : Vector Prop n :=
  Vector.ofFn (fun i => x.getLsbD (i.val + 1) || !x.getLsbD (i.val))

example {x : BitVec 17} : (SAT_ex1 x).foldl And True := by
  simp [SAT_ex1, Vector.ofFn, Array.ofFn_succ]
  bv_decide

gives you a counter example

[Aatman Supkar]

What does one do in more complicated situations?

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Analysis.RCLike.Basic
import Std.Tactic.BVDecide

universe u
set_option maxHeartbeats 2000000

/-! This file defines the notion of `GraphBoxicity` of a graph. It then proves the equivalence of a statement of the kind `GraphBoxicity G ≤ k` to a SAT expression depending on `G` and `k`. Finally, a `SimpleGraph` on the power set of `{1, 2, ... n}` is defined, where two subsets are adjacent if and only if one contains the other. An upper bound for the `GraphBoxicity` of these graphs is known: https://arxiv.org/abs/2501.16233. We prove a lower bound in the case of `n = 4` by using Lean's inbuilt SAT solver. -/

/-- We define an interval to just be a pair of points. If start > finish, we just have an empty interval. Meant to be treated as closed intervals. -/
structure Interval (α : Type u) [LinearOrder α] where
  start : α
  finish : α

/-- Boxes need to be 'axis-parallel', and can thus be defined as a list of intervals. -/
abbrev Box (α : Type u) [LinearOrder α] n := List.Vector (Interval α) n

/-- Given two intervals of the same type, returns their intersection. -/
@[simp]
def IntervalIntersection {α : Type u} [LinearOrder α] (i j : (Interval α)) : Interval α:=
  {start := max i.start j.start, finish := min i.finish j.finish}

/-- Given two boxes of the same type, returns their intersection. -/
@[simp]
def BoxIntersection {α : Type u} [LinearOrder α] {n : ℕ} (b1 b2 : Box α n) : Box α n :=
  List.Vector.ofFn (fun i ↦ IntervalIntersection (b1.get i) (b2.get i))

/-- Hypothesis that characterises when a given interval is non-empty. -/
@[simp]
def nonempty_interval {α : Type u} [LinearOrder α] (i : Interval α) : Prop :=
  i.start ≤ i.finish

@[simp]
def nonempty_box {n : ℕ} {α : Type u} [LinearOrder α] (b : Box α n) : Prop :=
  ∀ i : Fin n, nonempty_interval (b.get i)

/-- Each vertex `v ∈ G` is mapped to a non-empty box of dimension `n` via `Map`. Two distinct vertices `u,v ∈ G` intersect if and only if their corresponding boxes `Map u, Map v` intersect. The resulting box representation is said to be of dimension `n`. -/
structure BoxRepresentation (α : Type u) [LinearOrder α] (m : ℕ) {n : ℕ} (G : SimpleGraph (Fin n)) where
  Map : Fin n → Box α m
  h1 (i : Fin n): nonempty_box (Map i)
  h2 : ∀ u v : Fin n, (u = v) ∨ (nonempty_box (BoxIntersection (Map u) (Map v)) ↔ G.Adj u v)

/-- The boxicity of a graph `G` is the smallest number of dimensions `n` needed for a box representation of dimension `n` to exist. -/
@[simp]
noncomputable def GraphBoxicity {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ :=
  sInf {m | ∃ f : Fin n → Box ℝ m, ∃ R : BoxRepresentation ℝ m G, R.Map = f}

/-- A discrete version of boxicity using `Fin n`. Is supposed to be the same as `GraphBoxicity`. -/
@[simp]
noncomputable def GraphBoxicity' {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ :=
  sInf {m | ∃ f : Fin n → Box (Fin (n + 1)) m, ∃ R : BoxRepresentation (Fin (n + 1)) m G, R.Map = f}

def fin_succ {n : ℕ} (i : Fin n) : Fin (n + 1) :=
  let successor := i.val + 1
  ⟨successor, Nat.add_lt_of_lt_sub i.prop⟩

/-- Graph boxicity equals its discrete variant on all graphs. -/
theorem graphboxicity_eq_graphboxicity' {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    GraphBoxicity G = GraphBoxicity' G := by
  sorry

def num_rep {n : ℕ} (x : BitVec (n + 1)) : List Prop := List.ofFn (fun i ↦
  if i < n then  ¬x[i] || x[i+1] else x[i])

def start_le_finish {n : ℕ} (x1 x2 : BitVec (n + 1)) : List Prop := List.ofFn (fun i ↦ (x1[i] || ¬ x2[i]))

def adj_rel {n : ℕ} (start1 start2 finish1 finish2 : BitVec (n + 1)) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (u v : Fin n) : Prop :=
  if u = v then True
  else if G.Adj u v then List.and (List.ofFn (fun i ↦
    (start1[i] || ¬ finish2[i]) && (finish1[i] || ¬start2[i])))
  else ¬ (List.and (List.ofFn (fun i ↦
    (start1[i] || ¬ finish2[i]) && (finish1[i] || ¬start2[i]))))

def sat_equiv {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (dim : ℕ) (start finish : List.Vector (List.Vector (BitVec (n+1)) dim) n) : Prop :=
  (List.foldl And True (List.ofFn fun u ↦
    List.foldl And True (List.ofFn fun d ↦
     List.foldl And True (num_rep ((start.get u).get d)) ∧
     List.foldl And True (num_rep ((finish.get u).get d)) ∧
     List.foldl And True (start_le_finish ((start.get u).get d) ((finish.get u).get d))))) ∧
     List.foldl And True (List.ofFn fun d ↦
       List.foldl And True (List.ofFn fun u ↦
        List.foldl And True (List.ofFn (
        fun v ↦ adj_rel ((start.get u).get d) ((start.get v).get d) ((finish.get u).get d) ((finish.get v).get d) G u v))))

/-- Proves that the boxicity being at most a certain value -/
theorem sat_if_boxicity {n : ℕ} (G : SimpleGraph (Fin n)) (dim : ℕ) [DecidableRel G.Adj] :
  GraphBoxicity' G ≤ dim → ∃ start finish : List.Vector (List.Vector (BitVec (n+1)) dim) n, sat_equiv G dim start finish := by sorry

/-- Interpret a `Fin (2^n)` as a subset of `{0, ..., n - 1}` via its bitvector representation. -/
def toSubset {n : ℕ} (x : Fin (2^n)) : BitVec n :=
  BitVec.ofNat n x.val

/-- Two subsets are adjacent iff one contains the other. -/
def subsetAdj {n : ℕ} (u v : Fin (2^n)) : Prop :=
  let uB := toSubset u
  let vB := toSubset v
  if u = v then False else uB &&& vB = uB ∨ uB &&& vB = vB

/-- The graph on `2^n` subsets of `{0, ..., n - 1}`, with edges for subset/superset pairs. -/
def subsetGraph (n : ℕ) : SimpleGraph (Fin (2^n)) where
  Adj := @subsetAdj n
  symm := by
    intro u v h
    unfold subsetAdj
    by_cases h1 : u = v
    rw [← h1] at h
    exfalso
    unfold subsetAdj at h
    simp_all
    intro uB vB
    split_ifs with h2
    simp_all only [not_true_eq_false]
    simp_all only [subsetAdj, ite_false]
    unfold uB vB
    rwa [BitVec.and_comm, Or.comm]
  loopless := by
    intro u
    unfold subsetAdj
    by_contra h
    dsimp at h
    split_ifs at h with h1
    have h2 : u = u := rfl
    contradiction

/-- Now we install a `DecidableRel` instance for `subsetAdj` -/
instance subsetAdj.decidableRel {n : ℕ} : DecidableRel ((subsetGraph n).Adj) :=
  fun u v ↦
    if h : u = v then
      isFalse (by simp [h, subsetAdj])
    else
      let uB := toSubset u
      let vB := toSubset v
      if h₁ : uB &&& vB = uB then
        isTrue (by simp [h, h₁, subsetGraph, subsetAdj, uB, vB])
      else if h₂ : uB &&& vB = vB then
        isTrue (by simp [h, h₂, subsetGraph, subsetAdj, uB, vB])
      else
        isFalse (by simp [h, h₁, h₂, subsetGraph, subsetAdj, uB, vB])

theorem box_sub_3_gt_1 : GraphBoxicity (subsetGraph 3) > 1 := by
  rw [graphboxicity_eq_graphboxicity']
  by_contra h
  rw [Nat.not_lt] at h
  have h1 : ∃ start finish : List.Vector (List.Vector (BitVec 9) 1) 8, sat_equiv (subsetGraph 3) 1 start finish := by
    apply sat_if_boxicity
    exact h

  bv_decide

I've tried various ways to format at line 147 (the blank line before the bv_decide) but nothing has quite worked...

[Henrik Böving]

Well there is certainly situations where you have to start writing your own lemmas to turn some structure into a bitvec formula, this is the case here.

[Aatman Supkar]

Could you give me some pointers? For example, in one of the unfold sequences I tried, I couldn't get rid of an if (which I believe came from adj_rel) despite me providing an instance of its decidability.

Say you had to deal with something this ugly, what would your rough workflow be?

[Henrik Böving]

I haven't dealt with the graph API before so I wouldn't know really

[Henrik Böving]

But in general you want to incrementally build lemmas that get you closer and closer to a pure bitvec/bool formulation of what you are trying to achieve, I don't quite know how to do that without digging a bit into how graphs work though