부분 집합 커버를 위한 최적화 모델

최근 뉴스레터 기사에서 나는 연구자들이 자신의 연구의 적용 가능성에 대해 어떻게 잘못된 정보를 제공하는지에 대해 불평했습니다. SAT 솔버를 예로 들었습니다. 사람들은 반응에서 흥미로운 예를 제공했지만, 나에게 새로운 것은 SAT의 확장인 SMT(Satisfiability Modulo Theories)의 개념이었습니다. SMT는 일반적인 SAT보다 더 실용적인 용도가 있는 것 같습니다(자세한 내용은 뉴스레터를 참조하세요). SMT 솔버를 탐색하고 싶었고, 마이크로소프트에서 개발한 오픈소스 SMT 솔버인 Z3에 도착했습니다.