N Queen 문제를 SAT solver 로 풀기

imyejin의 이미지

요즘 논리 증명 관련 도구를 사용해야 할 일이 있어서 짧은 연재를 시작할까 합니다.

그 첫째는 N Queen 문제를 SAT solver로 푸는 것입니다. 여기서 SAT는 요즘 고딩들이 우리나라를 탈출해서 미쿡으로 가려고 보는 그 시험이 아니라, 컴싸나 컴공 기초 이론 시간에 배우는 최초로 NP 완전 문제라고 증명된 부울 대수의 충족 가능성 문제 영어로는 boolean satisfiability problem 줄여서 SAT 라 부릅니다. 자세한 내용은 위키피디아 관련 항목 http://ko.wikipedia.org/wiki/충족_가능성_문제 를 참조하시기 바랍니다. 참고로, 이 글은 http://narnia.cs.ttu.edu/drupal/node/121 를 바탕으로 하여 제가 실습해 본 것을 정리한 내용입니다.

비록 SAT이 NP 완전 문제이긴 하지만, 많은 경우에 적절한 시간 안에 풀어낼 수 있고 SAT문제가 활용되는 영역은 실로 다양합니다. 현재 가장 SAT을 가장 산업적으로 활발하게 활용하고 있는 곳은 Electronic Design Automation (EDA) 업계일텐데 회로 설계가 논리적으로 동일한지 알아보는 Formal Equivalence Checking (FEV) 에 대표적으로 활용되고 있습니다. 역시 자세한 내용은 위키피디아 http://en.wikipedia.org/wiki/Formal_equivalence_checking 를 참고하시기 바랍니다.

하지만 컴싸 컴공 사람들은 전자회로가 나오면 골치아프니 N Queen 문제나 가지고 놀아보는 게 재미있을 거 같습니다. SAT 문제를 풀어주는 SAT solver들이 있는데 이런 SAT solver를 이용해서 우리가 알고 있는 여러가지 문제들을 SAT solver에게 풀라고 시켜볼 수 있습니다. SAT은 워낙 광범위하게 이용되고 있기 때문에 표준적으로 통용되는 DIMACS Challenge Satisfiability Suggested Format ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.dvi 이라는 문법이 있고, 대부분의 SAT solver는 이 문법을 입력으로 받아 처리할 수 있습니다.

이 강좌에서는 오픈소스로 제공되는 대표적인 SAT solver인 MiniSat http://minisat.se/ 을 이용하겠습니다. 데비안 계열 리눅스에서는 아마 apt-get install minisat2 라고 하시면 설치하실 수있을 것입니다. SAT solver 프로그램이나 라이브러리는 아주 많습니다만 데비안 리눅스에서 패키지로 제공되어 설치하기 쉬운 것은 minisat2 과 picosat 입니다.

그럼 이제부터 minisat2를 이용해 N Queen 문제를 풀어 보겠습니다. 입력은 DIMACS SAT 형식 중에서 CNF를 쓰도록 하겠습니다. 논리곱 표준형 Conjunctive Normal Form (CNF) 가 무엇인지는 http://ko.wikipedia.org/wiki/논리곱_표준형 을 참조하시기 바랍니다. 대략 명제 변수 혹은 부정 기호가 붙은 명제 변수를 논리합(logical or)으로만 엮은 절들을 논리곱으로 엮은 형식을 말합니다. 모든 명제논리의 명제는 논리곱 표준형으로 변환할 수 있습니다. DIMACS SAT 형식은 CNF 외에도 논리곱과 논리합을 자유로이 섞어 쓸 수 있는 형식도 있는데 그와 관련해서는 앞서 제시한 링크에 나온 satformat.dvi 파일을 참조하시기 바랍니다.

그럼 가장 간단한 경우인 2 queen 문제부터 풀어 봅시다. 보드 배열이 다음과 같이 되어 있고 여기에 퀸 두개를 서로 길을 방해하지 않고 놓을 수 있나 SAT solver로 알아보도록 합시다.

1 2
3 4

아시는 분들은 아시겠지만 당연히 할 수 없습니다. 일반적으로 N 퀸 문제는 N>3 일 때만 답을 찾을 수 있거든요. 아래 프로그램에서 어떤 숫자는 그 숫자에 해당하는 보드 위치에 퀸이 있다는 것을 뜻하고 앞에 마이너스가 붙으면 그 명제의 부정 즉 그 숫자에 해당하는 보드 위치에 퀸이 없다는 것을 뜻합니다.

c 이 줄은 주석 줄입니다 줄의 첫 글자가 c 이면 주석이 됩니다
c 주석 이후 첫 줄에는 p cnf <명제변수개수> <절개수> 를 쓰고
c 그 다음 줄부터는 CNF의 각 절을 나열하는데 각 절은 0으로 구분합니다.
c 맨 끝에는 0을 쓸 필요가 없으며 각 절을 0으로 구분하기 때문에
c 굳이 줄바꿈을 할 필요가 없지만 가독성을 위해, 그리고 간혹 SAT solver 중에
c 한 줄에 하나씩만 입력을 받거나 맨 끝에 꼭 0이 오는 것으로 가정하고 만든
c SAT sovler 도 있을 수 있으므로 한 줄에 한 절씩 적고 맨 마지막 절 다음에도
c 0 으로 끝내는 것울 추천합니다.
p cnf 4 10
1 2 0
3 4 0
-1 -2 0
-3 -4 0
1 3 0
2 4 0
-1 -3 0
-2 -4 0
-1 -4 0
-2 -3 0

첫째와 둘째 줄은 한 가로행에 적어도 하나씩은 퀸을 놓아야 한다는 조건입니다. 예를 들면 1 2 0 은 1에 퀸이 있거나 2에 퀸이 있어야 한다는 것이죠. 셋째와 넷째 줄은 한 줄에 하나 이상의 퀸이 올 수 없다는 조건을 나타냅니다. -1 -2 0 의 경우 1과 2가 동시에 참이어 버리면 전체가 거짓이 되죠 왜냐하면, -1 -2 0 은 (NOT p1) OR (NOT p2) 를 뜻하니까요. 다섯번째 줄부터 여덟번째 줄은 세로열에 대한 조건이고, 나머지는 대각선에 대한 조건입니다. 위 파일을 q2.cnf로 저장하고 minisat2 로 이를 실행하면 다음과 같이 만족하는 해가 없다는 예상대로의 답변이 나옵니다. q2.out 은 minisat2 프로그램이 SAT 에 대한 출력 결과를 쓰는 파일입니다.

user@host:~$ minisat2 q2.cnf q2.out
This is MiniSat 2.0 beta
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:  4                                                    |
|  Number of clauses:    10                                                   |
|  Parsing time:         0.00         s                                       |
restarts              : 0
conflicts             : 0              (0 /sec)
decisions             : 0              ( nan % random) (0 /sec)
propagations          : 1              (250 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 4.07 MB
CPU time              : 0.004 s
 
UNSATISFIABLE
user@host:~$ cat q2.out 
UNSAT

3, 4, 5, 6, 7, 8, 9, 10 퀸 등 더 큰 N Queen 문제에 대해 손으로 일일이 cnf 파일을 생성하는 것은 너무 노가다이기 때문에 다음과 같이 하스켈로 조건을 계산해서 cnf 파일을 자동으로 생성하는 스크립트를 짰습니다. n = 8 로 주었기 때문에 8 퀸 문제를 풉니다. (커맨드 라인 옵션으로 받게 할 수도 있지만 귀찮아서 패스 ~~~~)

-- vim: expandtab: ai:
import List
 
data Atom a = F a | T a deriving (Eq,Show,Read)
 
varAtom (F x) = x
varAtom (T x) = x
 
exists xs = map T xs
 
existsAtMost1 []     = error "existsAtMost1: arg should not be an empty list"
existsAtMost1 [x]    = []
existsAtMost1 (x:xs) = [[F x,F y] | y<-xs] ++ existsAtMost1 xs
 
horizontals n = [map (+(k*n)) [1..n] | k<-[0..n-1]]
verticals n = [take n (iterate (+n) k) | k<-[1..n]]
diagonalPairs n = do g1 <- [1..n^2]
                     g2 <- [g1+1..n^2]
                     let (y1,x1) = (g1-1) `quotRem` n
                         (y2,x2) = (g2-1) `quotRem` n
                     if abs(x1-x2)==abs(y1-y2) then return [g1,g2] else fail ""
 
constraints n = map exists hs ++ concatMap existsAtMost1 hs
             ++ map exists vs ++ concatMap existsAtMost1 vs
             ++ concatMap existsAtMost1 ds
              where
                hs = horizontals n
                vs = verticals n
                ds = diagonalPairs n
 
-- DIMACS CNF
constraints2DIMACScnf cs =
  "p cnf "++show n++" "++show(length cs)++"\n" ++
  concat (intersperse " 0\n" (map showCNFclause cs)) ++ " 0"
  where n = (maximum $ concatMap (map varAtom) cs) :: Int
 
showCNFclause = concat . intersperse " " . map showAtom
 
showAtom (T x) = show x
showAtom (F x) = show (-x)
 
coord2num n (x,y) | x `inRange` (1,n) && y `inRange` (1,n) = x + n*y
 
inRange x (a,b) = a <= x && x <= b
 
n = 8
 
main = putStr $ constraints2DIMACScnf $ constraints n

위 하스켈 스크립트를 NQueenCNF.hs 로 저장하여 다음과 같이 CNF 파일을 생성하여 돌려보면 역시 예상대로 해가 있다고 나옵니다.

user@host:~$ runhaskell NQueenCNF.hs > q8.cnf
user@host:~$ minisat2 q8.cnf q8.out
This is MiniSat 2.0 beta
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:  64                                                   |
|  Number of clauses:    744                                                  |
|  Parsing time:         0.00         s                                       |
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
|         0 |      64      744     1584 |      248        0    nan |  0.000 % |
===============================================================================
restarts              : 1
conflicts             : 21             (5250 /sec)
decisions             : 43             (0.00 % random) (10750 /sec)
propagations          : 347            (86750 /sec)
conflict literals     : 341            (1.45 % deleted)
Memory used           : 4.06 MB
CPU time              : 0.004 s
 
SATISFIABLE
user@host:~$ cat q8.out 
SAT
-1 -2 -3 4 -5 -6 -7 -8 -9 10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 23 -24 -25 -26 27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 38 -39 -40 -41 -42 -43 -44 -45 -46 -47 48 -49 -50 -51 -52 53 -54 -55 -56 57 -58 -59 -60 -61 -62 -63 -64 0

n=2 일때와 달리 이번에는 만족하는 해가 있다고 하고 그걸 하나 보여줍니다. 결과로 나온 숫자를 8개씩 끊어서 다음과 같이 보기 좋게 배열해서 확인해 보면 정말 N Queen 문제의 해라는 걸 확인해 볼 수 있습니다.

 -1  -2  -3   4  -5  -6  -7  -8
 -9  10 -11 -12 -13 -14 -15 -16
-17 -18 -19 -20 -21 -22  23 -24
-25 -26  27 -28 -29 -30 -31 -32
-33 -34 -35 -36 -37  38 -39 -40
-41 -42 -43 -44 -45 -46 -47  48
-49 -50 -51 -52  53 -54 -55 -56
 57 -58 -59 -60 -61 -62 -63 -64

SAT 방식의 문제 해결 방법은 이와 같이 다양한 문제를 하나의 일반적인 SAT solver를 통해서 풀 수 있다는 장점이 있습니다. 하지만 특정한 문제 하나하나만을 확인해 볼 수 있지 일반적으로 N>3 에 대해 N Queen 문제의 해가 있다는 증명은 하지 못합니다. 이러한 증명을 자동으로 할 수 있는 자동 증명 Automated Theorem Proving (ATP) http://en.wikipedia.org/wiki/Automated_theorem_proving 기법이 있는데 다음 연재는 이에 대해 알아보도록 하겠습니다.

Forums: 
나그네나그네의 이미지

기대됩니다 :)

kkb110의 이미지

안녕하세요 재미있게 잘 보았습니다!
Sat Solver라는것을 이 글로 처음 접해보네요.

그런데 저는 보자마자 먼저 생각나는게.. hash function breaking이네요.
어떤 hash function이든지.. shift,addition,xor,... 등등의 연산을 반복하는게 기본 골격인데
bit단위로 분해해봤을때 하나의 큰 boolean expression으로 표현할 수가 있으니까요.
그리고 역시나.. 'sat solver hash function'으로 구글링을 해보니 잡히는게 좀 있군요.

유익한 글 감사합니다 ^^

JuEUS-U의 이미지

잘 읽었습니다. ^^

차리서의 이미지

언제나 좋은 글 감사드립니다. 특히 정리 증명에 관한 글은 무척 기대됩니다.

PS: 그냥 대충 경험적으로 드리는 말씀이라 저도 자신 없지만, 대체로 satisfiability라는 표현을 더 많이 쓰지 않던가요? @.@

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

imyejin의 이미지

satisfiability 가 파이어폭스가 사용하는 사전에 등록이 안 되어 있어서 빨간줄이 그어져서 반사적으로 우클릭해서 첫번째 나오는 걸 그냥 클릭하니까 sustainability 가 되어 버렸군요 -.-;; 수정하였습니다.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

wodnrrns의 이미지

유익한 글 감사합니다.

hyunmin90의 이미지

유익한 글이내요 .ㅎ 전 아직 공부좀 해야겠습니다 ㅎㅎ

죠커의 이미지

CNF가 이것이었군요. 옛날에 배운 것인데 명칭도 잊고 있었습니다.

Quote:
셋째와 넷째 줄은 한 줄에 하나 이상의 퀸이 올 수 없다는 조건을 나타냅니다. -1 -2 0 의 경우 1과 2가 동시에 참이어 버리면 전체가 거짓이 되죠 왜냐하면, -1 -2 0 은 (NOT p1) AND (NOT p2) 를 뜻하니까요.

여기에선 (NOT p1) OR (NOT p2)가 아닐까 싶습니다. AND라면 퀸은 어디에도 존재하지 못하겠죠.

1 2 0   ; p1 OR p2                  and...
3 4 0   ; p3 OR 4                   and...
-1 -2 0 ; (NOT p1) or (NOT p2)      and....
-3 -4 0 ; (NOT p3) or (NOT p4)      an...
1 3 0   ; p1 OR p3                  a...
2 4 0   ; p2 OR p4                  ..
-1 -3 0 ; (NOT p1) OR (NOT p3)      ..
-2 -4 0 ; (NOT p2) OR (NOT p4)      ..
-1 -4 0 ; (NOT p1) OR (NOT p4)      ..
-2 -3 0 ; (NOT p2) OR (NOT p3)      ..

위와 같은 내용이 맞나요? :)

- 죠커's blog / HanIRC:#CN

imyejin의 이미지

한줄 안에 있는 명제변수끼리는 OR로 묶여 있고, 각 줄들이 AND로 묶여 있는 것이죠. 지적 감사합니다. 수정하였습니다.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

트비터의 이미지

소스만 고치면 Nqueen 문제와 유사한 문제에도 응용할수 있겠군요.

트비터의 이미지

따라서 P=NP입니다.

imyejin의 이미지

전북대에서 매년 입시철만 되면 언론에 내보내는 그거 말고 다른걸로요.

근데 전북대 건은 P=/=NP였던 것으로 기억하는데 그럼 그것도 아닐테고 하여간 출처를 밝혀 주십시오.

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

트비터의 이미지

크리에이티브 커먼즈 저작자표시-동일조건변경허락 3.0으로 배포하는데 동의해 주시면 됩니다.


한국어
위키책

CCCP

pogusm의 이미지

좋은글 재밌게 보았습니다.

그런데, 혹시 http://kldp.org/node/128209 이 링크에 있는 저의 문제를 cnf 로 만들고,
minisat2 으로 해답을 찾을 수 있을까요?

조언좀 해주세요~

댓글 달기

Filtered HTML

  • 텍스트에 BBCode 태그를 사용할 수 있습니다. URL은 자동으로 링크 됩니다.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>
  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.

BBCode

  • 텍스트에 BBCode 태그를 사용할 수 있습니다. URL은 자동으로 링크 됩니다.
  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param>
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.

Textile

  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • You can use Textile markup to format text.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>

Markdown

  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • Quick Tips:
    • Two or more spaces at a line's end = Line break
    • Double returns = Paragraph
    • *Single asterisks* or _single underscores_ = Emphasis
    • **Double** or __double__ = Strong
    • This is [a link](http://the.link.example.com "The optional title text")
    For complete details on the Markdown syntax, see the Markdown documentation and Markdown Extra documentation for tables, footnotes, and more.
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>

Plain text

  • HTML 태그를 사용할 수 없습니다.
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.
  • 줄과 단락은 자동으로 분리됩니다.
댓글 첨부 파일
이 댓글에 이미지나 파일을 업로드 합니다.
파일 크기는 8 MB보다 작아야 합니다.
허용할 파일 형식: txt pdf doc xls gif jpg jpeg mp3 png rar zip.
CAPTCHA
이것은 자동으로 스팸을 올리는 것을 막기 위해서 제공됩니다.