minisat 모든 SAT 솔루션을 효율적으로 찾는 방법

Question

이 link에 설명 된 방법을 사용하여 모든 솔루션을 찾는 방법을 찾았습니다.

정상적으로 작동하지만 느립니다. i_e 시작부터 제약 조건을 다시 계산할 때 이전 계산을 활용하지 않습니다.

이제이 link에서 MiniSat을 라이브러리로 사용하여 모든 솔루션을 찾는보다 효율적인 방법을 발견했습니다. 그러나 방법은 거기에서 기술되지 않는다.

모든 SAT 솔루션을 효율적으로 찾을 수있는 적절한 문서를 가르쳐 주시겠습니까?

감사합니다.

Answer 1

모든 SAT 솔루션을 찾는 더 효율적인 방법은 Yu, Subramanyan, Tsiskaridze 및 Malik의 논문 "All-SAT using Minimal Blocking Clauses"에 설명되어 있습니다.

반복적으로 솔루션을 찾고 차단 조항을 추가하는 기본 전략은 동일하지만 차단 조항은 크기를 줄이는 새로운 아이디어를 사용하여 생성됩니다. 생성 된 블로킹 절은 일반적인 순진한 부분 할당보다 작으므로 반복마다보다 많은 양의 할당이 포함되므로 열거 프로세스가 빨라집니다.

내가 아는 한,이 문서에 포함 된 아이디어를 공개적으로 구현하지 않고 다운로드하여 실행할 수 있습니다.