Binairo Puzzle

비나이로 퍼즐

소개

이 프로젝트는 Takuzu라고도 불리는 Binairo 퍼즐(여기서는 온라인 게임 참조)을 해결하는 것으로 구성되며 다음과 같이 설명됩니다. 흰색 원이나 검은색 원을 포함할 수 있는 nxn개 셀의 격자가 있습니다. 초기 구성에서는 일부 셀 값을 제공하고 나머지는 다음 규칙에 따라 원으로 채워야 합니다.

• 각 행과 각 열에는 각 색상의 동일한 수의 원이 포함되어야 합니다. 즉, 각 사례의 n/2 인스턴스가 포함되어야 합니다.

• 어떤 방향(수직 또는 수평)으로든 동일한 색상의 원이 2개 이상 연속해서 있을 수 없습니다.

• 동일한 구성에는 두 개의 행이나 두 개의 열이 있을 수 없습니다.

초기 구성의 예와 해당 솔루션은 아래에서 볼 수 있습니다.

구현

시나리오를 SAT 문제와 ASP 프로그램으로 인코딩합니다.

이는 각 셀에 '0'(흰색 원), '1'(검은색 원) 또는 '.' 문자가 포함된 초기 그리드가 있는 ASCII 파일을 사용합니다. (채울 빈 셀) 첫 번째 줄에는 행과 열의 수를 지정하는 짝수 n>=2가 포함되어 있습니다(정사각형 격자가 있음). 예를 들어, 위 그림의 예는 다음과 같이 표현됩니다.

 6
......
.11.0.
01....
....00
.1....
0..1..

이 프로그램은 솔루션을 얻기 위해 ASP를 사용할 때 DIMACS 파일을 생성하고 SAT를 사용할 때 clasp 에 대한 외부 호출을 수행하거나 ASP를 사용할 때 clingo를 호출 합니다. 또한 다음과 같이 다시 출력을 디코딩하고 전체 솔루션을 인쇄합니다.

 100110
011001
010011
101100
110010
001101

실행

기본적으로 ASP를 사용하며 예제 폴더에는 다양한 크기(6, 8, 10, 14, 20)의 벤치마크 세트가 포함되어 있습니다. 여기서 domX.txt는 입력 파일이고 solX.txt는 해당 솔루션입니다.

 ./binairo.py [-h] [-a] [-c input] input

-h            show this help message and exit
-a            use ASP to solve
-c            compare the result with this file
-input        route of the binairo puzzle instance