sat_solver.gleam

sat_solver.gleam

// This heavily borrows (and is essentialy just a port) of https://andrew.gibiansky.com/blog/verification/writing-a-sat-solver/
import gleam/io
import gleam/list
import gleam/int
import gleam/option.{None, Option, Some}

type Expr {
  Var(Int)
  And(Expr, Expr)
  Or(Expr, Expr)
  Not(Expr)
  Const(Bool)
}

const example = [[1, 2, 3], [3, 4], [1, 5]]

pub fn main() {
  let expr = expr_from_dnf(example)
  io.debug(satisfiable(And(Var(1), Not(Var(1))), []))
  io.debug(satisfiable(expr, []))
  io.debug(all_satisfiable_scenarios(expr, []))
}

fn un_const(expr: Expr) -> Bool {
  assert Const(c) = expr
  c
}

fn all_satisfiable_scenarios(expr: Expr, acc: List(List(Int))) {
  case satisfiable(expr, []) {
    Some(scenario) ->
      all_satisfiable_scenarios(
        And(Not(expr_from_clause(scenario)), expr),
        [scenario, ..acc],
      )
    None -> acc
  }
}

fn satisfiable(expr: Expr, acc: List(Int)) -> Option(List(Int)) {
  case free_variable(expr) {
    None ->
      case un_const(expr) {
        True -> Some(acc)
        False -> None
      }
    Some(v) -> {
      let true_guess = simplify(guess_variable(expr, v, True))
      let false_guess = simplify(guess_variable(expr, v, False))
      option.lazy_or(
        satisfiable(true_guess, [v, ..acc]),
        fn() { satisfiable(false_guess, [v * -1, ..acc]) },
      )
    }
  }
}

fn simplify(expr: Expr) -> Expr {
  case expr {
    Const(c) -> Const(c)
    Var(v) -> Var(v)
    Not(e) ->
      case simplify(e) {
        Const(c) -> Const(!c)
        e -> Not(e)
      }
    Or(x, y) -> {
      let es =
        list.filter([simplify(x), simplify(y)], fn(v) { v != Const(False) })
      case es {
        [] -> Const(False)
        [Const(True)] -> Const(True)
        [Const(True), _] -> Const(True)
        [_, Const(True)] -> Const(True)
        [e] -> e
        [e1, e2] -> Or(e1, e2)
      }
    }
    And(x, y) -> {
      let es =
        list.filter([simplify(x), simplify(y)], fn(v) { v != Const(True) })
      case es {
        [] -> Const(True)
        [Const(False)] -> Const(False)
        [Const(False), _] -> Const(False)
        [_, Const(False)] -> Const(False)
        [e] -> e
        [e1, e2] -> And(e1, e2)
      }
    }
  }
}

fn guess_variable(expr: Expr, replacing_var: Int, val: Bool) -> Expr {
  case expr {
    Var(var) if var == replacing_var -> Const(val)
    Var(var) -> Var(var)
    Not(e) -> Not(guess_variable(e, replacing_var, val))
    Or(x, y) ->
      Or(
        guess_variable(x, replacing_var, val),
        guess_variable(y, replacing_var, val),
      )
    And(x, y) ->
      And(
        guess_variable(x, replacing_var, val),
        guess_variable(y, replacing_var, val),
      )
    Const(c) -> Const(c)
  }
}

fn expr_from_dnf(clauses: List(List(Int))) {
  option.unwrap(
    list.fold(
      clauses,
      None,
      fn(maybe_expr: Option(Expr), clause: List(Int)) {
        case maybe_expr {
          None -> Some(expr_from_clause(clause))
          Some(expr) -> Some(Or(expr, expr_from_clause(clause)))
        }
      },
    ),
    Const(False),
  )
}

fn expr_from_clause(clause: List(Int)) {
  option.unwrap(
    list.fold(
      clause,
      None,
      fn(maybe_expr: Option(Expr), var: Int) {
        let actual_var = case var {
          var if var < 0 -> Not(Var(int.absolute_value(var)))
          var -> Var(var)
        }

        case maybe_expr {
          None -> Some(actual_var)
          Some(expr) -> Some(And(expr, actual_var))
        }
      },
    ),
    Const(False),
  )
}

fn free_variable(expr: Expr) -> Option(Int) {
  case expr {
    Const(_) -> None
    Var(int) -> Some(int)
    Not(e) -> free_variable(e)
    Or(x, y) -> option.lazy_or(free_variable(x), fn() { free_variable(y) })
    And(x, y) -> option.lazy_or(free_variable(x), fn() { free_variable(y) })
  }
}