SAT in HVM

SAT.hvml

// Boolean constructors and functions
T           = λt λf t
F           = λt λf f
(Id a)      = a
(Not a)     = λt λf (a f t)
(And a b)   = (a λx(x) λx(F) b)
(Or a b)    = (a λx(T) λx(x) b)
(Or3 a b c) = (Or a (Or b c))
data List = (Cons head tail) | Nil

// Pretty prints a bool
(B x) = (x 1 0)

// Pretty-prints a 16-var solution
(V16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x) = (x λt(t
  (B x0) (B x1) (B x2) (B x3)
  (B x4) (B x5) (B x6) (B x7)
  (B x8) (B x9) (B x10) (B x11)
  (B x12) (B x13) (B x14) (B x15)
) 0)

(Carry x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x) = (x (Cons λt(t
  (B x0) (B x1) (B x2) (B x3)
  (B x4) (B x5) (B x6) (B x7)
  (B x8) (B x9) (B x10) (B x11)
  (B x12) (B x13) (B x14) (B x15)
) Nil) Nil)

// A random 3-SAT instance with 16 variables
(Foo x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) =
  (Carry x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
  (And (Or3 x12 x8 (Not x11))
  (And (Or3 (Not x10) (Not x2) (Not x8))
  (And (Or3 x11 (Not x9) x4)
  (And (Or3 x10 x1 (Not x8))
  (And (Or3 (Not x9) x0 x5)
  (And (Or3 (Not x4) (Not x4) x13)
  (And (Or3 (Not x1) (Not x4) x11)
  (And (Or3 (Not x2) x14 (Not x13))
  (And (Or3 x13 (Not x8) (Not x7))
  (And (Or3 x13 (Not x1) x7)
  (And (Or3 (Not x8) x4 x8)
  (And (Or3 x5 (Not x0) x12)
  (And (Or3 x1 x0 (Not x3))
  (And (Or3 x3 x14 (Not x13))
  (And (Or3 x9 (Not x12) (Not x11))
  (And (Or3 x8 (Not x14) (Not x5))
  (And (Or3 (Not x7) (Not x9) (Not x15))
  (And (Or3 x15 x11 x2)
  (And (Or3 (Not x2) (Not x14) (Not x7))
  (And (Or3 (Not x14) x3 (Not x3))
  (And (Or3 x3 (Not x15) x1)
  (And (Or3 (Not x0) x0 x13)
  (And (Or3 (Not x8) (Not x3) x12)
  (And (Or3 x12 (Not x1) x7)
  (And (Or3 x2 (Not x14) (Not x0))
  (And (Or3 x6 (Not x5) x1)
  (And (Or3 (Not x12) x3 (Not x3))
  (And (Or3 (Not x1) (Not x12) (Not x5))
  (And (Or3 x11 x10 x6)
  (And (Or3 x15 x6 x9)
  (And (Or3 (Not x15) x3 (Not x9))
  (And (Or3 (Not x11) x1 x8)
  (And (Or3 x9 (Not x14) x14)
  (And (Or3 (Not x10) (Not x2) x2)
  (And (Or3 x5 x14 (Not x2))
  (And (Or3 (Not x11) x12 x2)
  (And (Or3 x1 x11 (Not x2))
  (And (Or3 x8 (Not x6) (Not x7))
  (And (Or3 x13 x9 (Not x10))
  (And (Or3 x0 x8 (Not x8))
  (And (Or3 (Not x10) x9 (Not x0))
  (And (Or3 (Not x14) (Not x7) (Not x12))
  (And (Or3 x9 x12 (Not x10))
  (And (Or3 (Not x7) (Not x15) x13)
  (And (Or3 x0 (Not x2) x13)
  (And (Or3 x12 (Not x9) (Not x0))
  (And (Or3 (Not x10) x8 (Not x1))
  (And (Or3 x4 x5 (Not x14))
  (And (Or3 (Not x0) x5 (Not x7))
  (And (Or3 (Not x1) (Not x12) x10)
  (And (Or3 x0 x15 x9)
  (And (Or3 (Not x10) x3 (Not x2))
  (And (Or3 (Not x7) (Not x15) x6)
  (And (Or3 (Not x1) x4 (Not x5))
  (And (Or3 x12 (Not x8) x2)
  (And (Or3 x4 x7 (Not x5))
  (And (Or3 (Not x9) (Not x0) (Not x10))
  (And (Or3 x12 x1 (Not x2))
  (And (Or3 x11 x14 (Not x11))
  (And (Or3 x15 x5 x10)
  (And (Or3 (Not x6) x14 x3)
  (And (Or3 (Not x11) x11 x1)
  (And (Or3 (Not x15) x0 x7)
       (Or3 x14 (Not x3) (Not x2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

List.concat = λa λb match a {
	(Cons h t): (Cons h Nil)
	Nil: b
}

Oper = λa λb (List.concat a b)

SOr0 = λx dup#A0 x0 x1 = x; (Oper x0 x1)
SOr1 = λx dup#A1 x0 x1 = x; (Oper x0 x1)
SOr2 = λx dup#A2 x0 x1 = x; (Oper x0 x1)
SOr3 = λx dup#A3 x0 x1 = x; (Oper x0 x1)
SOr4 = λx dup#A4 x0 x1 = x; (Oper x0 x1)
SOr5 = λx dup#A5 x0 x1 = x; (Oper x0 x1)
SOr6 = λx dup#A6 x0 x1 = x; (Oper x0 x1)
SOr7 = λx dup#A7 x0 x1 = x; (Oper x0 x1)
SOr8 = λx dup#A8 x0 x1 = x; (Oper x0 x1)
SOr9 = λx dup#A9 x0 x1 = x; (Oper x0 x1)
SOrA = λx dup#AA x0 x1 = x; (Oper x0 x1)
SOrB = λx dup#AB x0 x1 = x; (Oper x0 x1)
SOrC = λx dup#AC x0 x1 = x; (Oper x0 x1)
SOrD = λx dup#AD x0 x1 = x; (Oper x0 x1)
SOrE = λx dup#AE x0 x1 = x; (Oper x0 x1)
SOrF = λx dup#AF x0 x1 = x; (Oper x0 x1)
// Finds a solution by trying all superposed applications of Foo
Main = 
(SOr0
(SOr1
(SOr2
(SOr3
(SOr4
(SOr5
(SOr6
(SOr7
(SOr8
(SOr9
(SOrA
(SOrB
(SOrC
(SOrD
(SOrE
(SOrF
(Foo
  {#A0 T F} {#A1 T F} {#A2 T F} {#A3 T F}
  {#A4 T F} {#A5 T F} {#A6 T F} {#A7 T F}
  {#A8 T F} {#A9 T F} {#AA T F} {#AB T F} 
  {#AC T F} {#AD T F} {#AE T F} {#AF T F}
)))))))))))))))))

// Solution found in the output:
// (b 0 1 0 1 0 0 1 1 1 0 1 0 1 1 0 1)