Naive SAT solver in Coq

NaiveSatSolver.v

From Coq Require Import Bool.

Ltac solve_sat_naive :=
  repeat multimatch goal with
  | [|- exists _ : bool, _] => exists true
  | [|- exists _ : bool, _] => exists false
  end; reflexivity.

Example ex_01 : exists x y, x && negb y = true.
Proof. solve_sat_naive. Qed.

Example ex_02 : exists x y z, x && negb y || z = false.
Proof. solve_sat_naive. Qed.

Example ex_e1 : exists x, x && negb x = true.
Proof. Fail solve_sat_naive. Abort.

Print ex_01.
(*
  ex_01 =
  ex_intro (fun x => exists y, x && negb y = true) true
    (ex_intro (fun y => true && negb y = true) false
       eq_refl)
       : exists x y, x && negb y = true
*)