smt

수식의 만족 가능성을 판별하는 문제로, 소프트웨어 및 하드웨어의 형식 검증에 널리 사용되는 핵심 기법이다. 복잡한 논리 구조의 오류를 찾는 데 사용된다.