제약을 만족하는 값 찾기
여러 절을 모두 참으로 만드는 불리언 변수 배정이 있는지 확인한다. 원래 문제가 프로그램의 오류 조건이라면 해당 조건을 논리식으로 옮기는 앞단 작업이 필요하다. solver가 반환한 모델이 어떤 변수에 대응하는지 유지해야 결과를 이해할 수 있다. 보조 변수를 실제 입력과 혼동하지 않는다.
가정과 자원 제한
API에서 변수를 만들고 절을 추가하며 특정 가정 아래에서 풀이를 요청할 수 있다. 자원 제한을 적용한 풀이와 중단 요청도 제공한다. 제한된 실행에서는 미확정 상태를 처리해야 하며 단순한 참과 거짓으로 뭉뚱그리지 않는다. 모델 값은 만족하는 결과를 얻은 뒤에 읽어야 한다.
구성과 재현성
저장소는 기본 solver와 단순화 기능을 더한 solver를 구분한다. 재시작이나 탐색 관련 설정이 수행 과정에 영향을 줄 수 있어 같은 입력이라도 실행 조건을 함께 확인한다. 도구를 수정하거나 다른 시스템에 넣을 때는 API의 상태 규칙과 빌드 구성을 유지한다. 프로그램 전체의 정확성과 입력 CNF의 만족 가능성은 별도의 문제다.
관련 문서
CaDiCaL / CryptoMiniSat / Kissat / Boolector