SatisfiableQ

SatisfiableQ[bf] gives True if a combination of values of variables exists that makes the Boolean function bf yield True.

SatisfiableQ[expr, {a1, a2, ...}] gives True if a combination of values of the ai exists that makes the Boolean expression expr yield True.

Examples

Check if formula is satisfiable:

SatisfiableQ[a && b]
(* True *)

Unsatisfiable formula:

SatisfiableQ[a && !a]
(* False *)

Please visit the official Wolfram Language Reference for more details.