한줄평
“SAT 문제를 직접 풀거나 솔버를 연구·응용하려는 개발자·연구자에게 적합합니다. 입력을 DIMACS 같은 전용 형식으로 만들어야 해 일반 용도는 아닙니다.”
이런 분께 SAT 문제를 풀거나 솔버를 응용하려는 개발자·연구자께
좋은 점
- 작고 빠른 고전 SAT 솔버
- 다른 솔버·연구의 기반이 될 만큼 검증됨
아쉬운 점
- 전용 입력 형식을 다뤄야 합니다
- 특정 문제 영역에 한정된 전문 도구
미니샛 소개
작고 단순하면서도 성능이 뛰어난 SAT(불 만족성 문제) 솔버입니다. 논리식이 참이 되는 변수 조합이 존재하는지 판정하며, 많은 후속 솔버와 연구의 바탕이 된 고전으로 꼽힙니다. 검증·최적화·인공지능 등에서 제약 문제를 SAT로 환원해 풀 때 씁니다. 명령줄에서 실행하는 도구이자 라이브러리입니다.
