# Boolean satisfiability problem

> 명제 논리식을 만족시키는 변수 집합이 존재하는지 검사하는 결정문제. 예를 들어 `a AND not B`는 `a`가 `TRUE`이고 `b`가 `FALSE`이면 참이므로 이 식은 "만족가능(satisfiable)"하다.

[명제 논리식](https://wiki.g15e.com/pages/Propositional%20logic%20formula.txt)을 만족시키는 변수 집합이 존재하는지 검사하는 [결정문제](https://wiki.g15e.com/pages/Decision%20problem.txt). 예를 들어 `a AND not B`는 `a`가 `TRUE`이고 `b`가 `FALSE`이면 참이므로 이 식은 "만족가능(satisfiable)"하다.

## See also

- [SAT solver](https://wiki.g15e.com/pages/SAT%20solver.txt)