fun SATsolver variables expr =
    let
        fun isVariableValid variable value variables = eval_variable variable variables = value
        handle InvalidVariable => true (* not yet 'removed' *)

        fun safeValueOf ((name, value)::tail) variable = if name = variable then SOME value
                                                         else safeValueOf tail variable
            | safeValueOf [] _ = NONE

        (* prune single variables *)
        fun findSingleVariables variables expr =
            case expr of
                Or [Variable v] => if isVariableValid v true variables then (Or [True], (v, true)::variables)
                                   else raise InvalidVariable
                | Or [Not (Variable v)] => if isVariableValid v false variables then (Or [Not False], (v, false)::variables)
                                           else raise InvalidVariable
                | True => (True, variables)
                | False => (False, variables)
                | Variable var => (case safeValueOf variables var of
                    SOME true => (True, variables)
                    | SOME false => (False, variables)
                    | NONE => (Variable var, variables))
                | Equiv (left_expr, right_expr) =>
                    let
                        val (left, variables) = findSingleVariables variables left_expr
                        val (right, variables) = findSingleVariables variables right_expr
                    in
                        (Equiv (left, right), variables)
                    end
                | Implies (left_expr, right_expr) =>
                    let
                        val (left, variables) = findSingleVariables variables left_expr
                        val (right, variables) = findSingleVariables variables right_expr
                    in
                        (Equiv (left, right), variables)
                    end
                | And expressions =>
                    let
                        val (expressions, variables) = kleisliMap findSingleVariables variables expressions
                    in
                        (And expressions, variables)
                    end
                | Or expressions =>
                    let
                        val (expressions, variables) = kleisliMap findSingleVariables variables expressions
                    in
                        (Or expressions, variables)
                    end
                | Not expr =>
                    let
                        val (expr, variables) = findSingleVariables variables expr
                    in
                        (Not expr, variables)
                    end

        fun selectVariable variables expr =
            let
            in
                case expr of
                    Equiv _ => NONE
                    | Implies _ => NONE
                    | And [] => NONE
                    | Or [] => NONE
                    | True => NONE
                    | False => NONE

                    | And expressions =>
                        let
                            (* can optimize by only taking first *)
                            val variables = compactMap $ map (selectVariable variables) expressions
                        in
                            case variables of
                                h::_ => SOME h
                                | [] => NONE
                        end
                    | Or expressions =>
                        let
                            (* can optimize by only taking first *)
                            val variables = compactMap $ map (selectVariable variables) expressions
                        in
                            case variables of
                                h::_ => SOME h
                                | [] => NONE
                        end
                    | Variable var => (case safeValueOf variables var of
                        SOME _ => NONE
                        | NONE => SOME var)
                    | Not expr => selectVariable variables expr
            end

        val (updatedExpr, variables) = findSingleVariables variables expr
        val simplified = simplify updatedExpr

        fun optToStr (SOME _) = "SOME" | optToStr NONE = "NONE";

(*      val _ = print $ toString expr
        val _ = print $ "\n"
        val _ = print $ toString $ updatedExpr
        val _ = print $ "\n"
        val _ = print $ varsToString $ variables
        val _ = print $ "\n"
        val _ = print $ toString $ simplified
        val _ = print $ "\n"*)
    in
        case simplified of
            True => SOME variables
            | And [] => SOME variables
            | False => NONE
            | Or [] => NONE
            | _ =>
                let
                    val var = selectVariable variables simplified
                in
                    (* why this doesn't work ???
                    case Option.map (fn var => SATsolver ((var, true)::variables) simplified) var of
                        SOME vars => vars
                        | NONE => (case Option.map (fn var => SATsolver ((var, false)::variables) simplified) var of
                            SOME vars => vars
                            | NONE => NONE)*)

                    (* this works just fine
                    case var of
                        SOME var => (case SATsolver ((var, true)::variables) simplified of
                            SOME vars => SOME vars
                            | NONE => (case SATsolver ((var, false)::variables) simplified of
                                SOME vars => SOME vars
                                | NONE => NONE))
                        | NONE => NONE*)

                    (* this seems the nicest *)
                    case var of
                        SOME var => mapNone (fn () => (SATsolver ((var, false)::variables) simplified))
                                            (SATsolver ((var, true)::variables) simplified)
                        | NONE => NONE
                end
    end
    handle InvalidVariable => NONE;