The Boolean Satisfiability Problem, also known as SAT, is a concept in logic and computer science of determining whether there exists an interpretation that satisfies a given Boolean formula.
SAT is the first problem that was shown to be [[NP-Complete]]. There is no known algorithm that efficiently solves each SAT problem, and it is generally believed that no such algorithm exists. This belief has no mathematical proof.
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem