논리식을 만족하는 배정
불리언 변수의 값을 정해 모든 조건을 동시에 참으로 만들 수 있는지 판단한다. 실제 프로그램이나 일정 문제를 풀려면 그 요구를 명제 논리식으로 옮기는 과정이 필요하다. solver의 결과가 정확해도 부호나 제약을 잘못 옮겼다면 원래 문제와 다른 답을 얻게 된다.
충돌을 학습하는 탐색
CDCL은 탐색 중 충돌에서 얻은 정보를 이용해 이후 탐색을 줄이는 SAT 방식이다. CaDiCaL은 이해하고 수정하기 쉬운 구현과 성능을 함께 추구한 프로젝트다. 특정 문제군의 성능을 모든 입력에 대한 우위로 일반화하지 않고 실제 대상 문제와 자원 조건에서 비교한다.
다른 도구의 부품으로 사용
실행 파일로 입력을 풀거나 라이브러리 API를 통해 제약과 질의를 전달할 수 있다. SMT solver 같은 상위 도구의 백엔드로도 활용된다. 명령행의 문제 형식과 라이브러리의 값 표현을 구분하고 모델 및 증명 자료가 필요한지 목적에 맞게 설정한다. 버전과 옵션 및 입력을 함께 보존해 다시 확인할 수 있도록 한다.
관련 문서
STP solver / Bitwuzla / Boolector / cvc5