CNF와 XOR 조건
명제 변수와 절로 표현한 제약을 만족하는 값이 있는지 찾는다. XOR 조건을 함께 표현할 수 있어 관련 구조가 많은 문제를 다룬다. 이름에 암호가 들어가지만 암호 구현을 자동으로 안전하게 만드는 도구는 아니다. 실제 요구를 제약으로 옮긴 뒤 결과를 원래 변수의 의미에 맞춰 해석해야 한다.
가정과 영구 조건의 차이
특정 풀이에만 적용하는 가정과 계속 유지할 절을 구분한다. 가정 아래에서는 해가 없어도 다음 질의에서 가정을 빼면 원래 문제의 해가 남을 수 있다. 같은 solver 객체를 반복 사용할 때 현재 어떤 조건이 남아 있는지 관리한다. 명령행과 라이브러리의 변수 번호 표현도 구분해 오류를 줄인다.
여러 해와 증명 자료
여러 해를 구하려면 찾은 배정을 제외하는 조건을 추가해 다시 푸는 방식을 사용할 수 있다. 원래 의미가 있는 변수와 변환용 보조 변수를 구분하지 않으면 같은 해처럼 보이는 결과가 반복될 수 있다. 필요하면 풀이 증명 자료를 생성해 별도 검사기로 확인한다. 빌드 옵션과 백엔드 및 입력을 함께 보존해 결과를 재현한다.
관련 문서
CaDiCaL / STP solver / Bitwuzla / Boolector