Naive SAT-solver in OC*ml 🤮

main.ml

(* propositional logic *)
(* https://t.me/keistash/148 *)

type expr
  = Lit of bool (* base case *)
  | Var of string (* base case *)
  | Not of expr
  | And of expr * expr
  | Or of expr * expr

(* takes the first variable *)
let rec pop : expr -> string option = function
  | Lit _ -> None
  | Var name -> Some name
  | Not x -> pop x
  | And (x, y) -> (match pop x with
    | None -> pop y
    | Some x' -> Some x')
  | Or (x, y) -> (match pop x with
    | None -> pop y
    | Some x' -> Some x')

let rec subst (e : expr) (name : string) (value : bool) : expr = match e with
  | Lit _ -> e
  | Var name' -> if name = name' then Lit value else e
  | Not x -> Not (subst x name value)
  | And (x, y) -> And (subst x name value, subst y name value)
  | Or (x, y) -> Or (subst x name value, subst y name value)

let rec eval : expr -> bool = function
  | Lit b -> b
  | Var name -> failwith ("free variable: " ^ name)
  | Not x -> not (eval x)
  | And (x, y) -> eval x && eval y
  | Or (x, y) -> eval x || eval y

let conj : expr = And (Lit true, Lit false)
let disj : expr = Or (Lit true, Lit false)
let ex : expr = And (conj, Var "x")

(* true = SAT; false = UNSAT *)
let rec solve (e : expr) : bool = match pop e with
  | None -> eval e
  | Some name ->
    let t = subst e name true in
    let f = subst e name false in
    solve t || solve f

(* SAT; A=true *)
(* A *)

(* SAT; A=true,B=true *)
(* A & B *)

(* SAT; sol1: A=true, B=false; sol2: A=false, B=true, sol3: A=true, B=true *)
(* A | B *)

(* SAT; sol1: A=true; sol2: A=false *)
(* !A | A *)

(* UNSAT *)
(* !A & A *)

(* ex = true && a *)
(* subst ex a true => true && true *)
(* subst ex a false => true && false *)

let () =
  let a = Var "a" in
  let b = Var "b" in
  let ex1 = a in
  let ex2 = And (a, b) in
  let ex3 = Or (a, b) in
  let ex4 = Or (Not a, a) in
  let ex5 = And (Not a, a) in
  print_endline (string_of_bool (solve ex1));
  print_endline (string_of_bool (solve ex2));
  print_endline (string_of_bool (solve ex3));
  print_endline (string_of_bool (solve ex4));
  print_endline (string_of_bool (solve ex5))