퍼즐의 SAT 제약 조건을 DNF에서 최적화

Question

현재 공감 형 표준 형식 (CNF)으로 입력되는 SAT 솔버로 퍼즐 "Kuromasu"을 해결하려고합니다.

Kuromasu에는 mxn 셀이 포함 된 직사각형 보드가 있습니다. 셀은 검정색 또는 흰색 중 하나입니다. 게임의 목표는 어떤 셀이 어떤 색인지 결정하는 것입니다. 일부 셀은 숫자를 포함합니다. 숫자가 포함 된 셀은 항상 흰색입니다. 숫자는 셀을 포함하여 얼마나 많은 세포가이 세포에서 볼 수 있어야하는지 알려줍니다. 같은 행과 열에있는 모든 흰색 셀이 첫 번째 검은 셀까지 표시됩니다. 나는 SAT 해결사가 이해하는 방법으로 블랙 필드의 위치를 ​​찾으려면이 제약을 수립 할 필요가

___________ 
| | |#| |2| <-- 2 cells including itself visible 
___________ 
| | |#| |#| 
___________ 
| |#|3| |#| <-- 3 cells including itself visible 
___________ 
| | | | | | 
___________ 

:

예 5 × 4 그리드, # 검은 셀을 나타냅니다. 번호가 매겨진 셀의 왼쪽, 오른쪽, 위쪽, 아래쪽으로 모든 셀을 이동하고 검정색으로 칠하면 제약 조건을 충족하는지 확인하여 번호 당 Disjunctive Normal Form (DNF) 버전을 생성 할 수 있습니다. 이것은 DNF에서 가능한 검은 색 별자리의 목록을 제공합니다. 셀마다 변수를 도입하여 게임을 인코딩합니다. 거짓이면 검정이고, 참이면 셀은 흰색입니다. 만 2 번호 제약 조건

________________ 
| 1| 2| 3| 4| 5| 
________________ 
| 6| 7| 8| 9|10| 
________________ 
|11|12|13|14|15| 
________________ 
|..|..| | | | 
________________ 

: 이하 합니다 (DIMACS 포맷들이 포지티브 대조로서 음수 거짓 변수 진정한 변수를 지정하기 때문에, 1 인덱스) 상기 필드의 모든 변수 위의 예는, 나는 다음을 생성합니다 :

___________ 
| | | | |2| <-- 2 cells including itself visible 
___________ 
| | | | | | 
___________ 
| | | | | | 
___________ 
| | | | | | 
___________ 

(-4 & -15) | (--10) (1)

이것은 제약 조건을 따라갈 수있는 두 가지 방법을 나타낸다. 그러나 이것을 SAT-Solver에 입력하려면 (식 1)을 CNF로 변환해야합니다. 작동하는 (순진) 변환기를 구현했지만 실제로 느리고 메모리 집약적 인 이유는 complexity이 CNF로 변환 되었기 때문입니다. 이를 수행하는 4 가지 이상의 방법이있는 제약 조건에 대해이를 수행하는 것은 실현 불가능합니다.

해 찾기에 직접 적용 할 수있는 방법으로 제약 조건을 공식화하는 방법은 무엇입니까? 가능한가? 나는 이것을 꽤 오랫동안 생각해 왔고 그것을 얻을 수 없다.

감사합니다.

Answer 1

위의 설명에서 언급 한 Tseytin 변환이 잘 작동합니다. 다른 사람이 필요로하는 경우를 대비해 다음은 Java의 일부 코드입니다.

: 이것은 Tseytin 변환의 전체 구현이 아니며, 입력이 이미 DNF 인 경우에만 작동합니다. 아래의 코드는 해킹 된 해법의 예입니다. 입력과 출력을 본질적으로 동일한 형식으로, 다른 해석으로 구현하는 것은 매우 유형 안전하지 않습니다. 필요에 따라 언제든지 수정할 수 있습니다.

편집 : 내 자신의 안전/학문 정직을 위해 마감일이 정해진 수업 과제가 끝난 후에 (1 월 8 일) 코드를 추가 할 것입니다.