the asymptotics of victor taelins sat solver

Stream: general

[Jared green]

is victor taelin still interested in determining the time complexity of his SAT solver for hvm? i wrote it in lean with an optimization (i wont try to prove termination):

-- i converted the sat solver algorithm using superpositions
--from https://gist.github.com/VictorTaelin/9061306220929f04e7e6980f23ade615
--(as i understand it) to the lambda calculus
--this algorithm is exactly DPLL with implicit unit propagation

--the input variables are given numbers so that splits are sorted.
inductive superposition
  where
  | just : Bool -> superposition
  | split : Nat -> Bool -> (superposition × superposition) -> superposition


namespace superposition

def seq (s1 s2 : superposition) : Bool :=
  match s1, s2 with
  | just a, just b => a = b
  | split n a (b, c),split m d (e, f) => n == m &&
    if a = d
    then seq b e && seq c f
    else seq b f && seq c e
  | _, _ => false

--a superposition of identical branches collapses to one
def converge (s : superposition) : superposition :=
  match s with
  | just a => just a
  | split n a (b, c) => match (converge b, converge c) with
    | (b, c) => if seq b c then b else split n a (b, c)


--these will place branches that can have true on them on the left side
def not  (s : superposition ) : superposition :=
  match converge s with
  | just a => just !a
  | split n a (b, c) => split n (!a) (not c, not b)

def and (s1 s2 : superposition) : superposition :=
  match converge s1, converge s2 with
  | just a, just b => just (a && b)
  | just false, _ => just false
  | just true,  t => t
  | _, just false => just false
  | t, just true => t
  | split n a (b, c), split m d (e, f) =>
    if n == m then
      if a = d then  split n a (and b e, and c f)
      else match converge (and b f), converge (and c e) with
      | just true, g => split n a (just true, g)
      | g, just true => split n (!a) (just true, g)
      | just false, g => split n (!a) (g, just false)
      | g, just false => split n a (g, just false)
      | g, h => if a then split n true (g, h) else split n true (h, g) --this makes the same match statement happen less
    else if n < m then split n a (and b s2, and c s2)
    else split m d (and e s1, and f s1)

def or (s1 s2 : superposition) : superposition :=
  match converge s1, converge s2 with
  | just a, just b => just (a || b)
  | just false, t => t
  | just true, _ => just true
  | t, just false => t
  | _, just true => just true
  | split n a (b, c), split m d (e, f) =>
    if n == m then
      if a = d then  split n a (or b e, or c f)
      else match converge (or b f), converge (or c e) with
      | just true, g => split n a (just true, g)
      | g, just true => split n (!a) (just true, g)
      | just false, g => split n (!a) (g, just false)
      | g, just false => split n a (g, just false)
      | g, h => if a then split n true (g, h) else split n true (h, g)
    else if n < m then split n a (or b s2, or c s2)
    else split m d (or e s1, or f s1)


--this is to get the negation normal form before attempting to find a solution,
--avoiding flipping the superpostions more than is necessary
inductive circuit
  where
  | vari : Nat -> circuit
  | Not : circuit -> circuit
  | And : circuit -> circuit -> circuit
  | Or : circuit -> circuit -> circuit

def normalize (c : circuit) : circuit :=
  match c with
  | circuit.vari n => circuit.vari n
  | circuit.Not (circuit.Not a) => normalize a
  | circuit.Not (circuit.vari n) => circuit.Not (circuit.vari n)
  | circuit.Not (circuit.And a b) => circuit.Or (normalize (circuit.Not a)) (normalize (circuit.Not b))
  | circuit.And a b => circuit.And (normalize a) (normalize b)
  | circuit.Not (circuit.Or a b) => circuit.And (normalize (circuit.Not a)) (normalize (circuit.Not b))
  | circuit.Or a b => circuit.Or (normalize a) (normalize b)

def tosuperposition (c : circuit) : superposition :=
  match normalize c with
  | circuit.vari n => split n true (just true,just false)
  | circuit.Not a => not (tosuperposition a)
  | circuit.And a b => and (tosuperposition a) (tosuperposition b)
  | circuit.Or a b => or (tosuperposition a) (tosuperposition b)

--gets the left brach. if there is a solution, the left branch is one
def leftpath (s : superposition) : List (Nat × Bool) :=
  match s with
  | just _ => []
  | split n a (b, _) => (n, a) :: leftpath b

def firstsolution (c : circuit) : Option (List (Nat × Bool)) :=
  match converge (tosuperposition c) with
  | just false => none
  | a => some (leftpath a)

def satisfiable (c : circuit) : Bool :=
  firstsolution c != none