[Python筆記]Pigeonhole Problem(鴿籠問題)以CNF檔案輸出

Outline

設想,總共有 n 隻鴿子和 m 個籠子,每一隻鴿子都要有一個籠子可以住,但每個籠子只能住一隻鴿子,請問對於這些鴿子和籠子,是否有適合的安排方式?雖然可能有很多種,但我們可以直接知道,當鴿子的數量比籠子還要多的時候,這個問題是無解的。

Variable

  • $n$,鴿子數量
  • $m$,籠子數量

Instruction

假設 3 隻鴿子在 3 個籠子裡,即 $n=3, m=3$ :

$ python pigeonhole.py
> Enter the number of pigeons(n):3
> Enter the number of holes(m):3
c
c number of pigeons(n): 3 ,number of holes(m): 3
c
p cnf 9 12
1 2 3 0
4 5 6 0
7 8 9 0
-1 -4 0
-1 -7 0
-4 -7 0
-2 -5 0
-2 -8 0
-5 -8 0
-3 -6 0
-3 -9 0
-6 -9 0

Detail

一隻鴿子一定住在任意一個鴿舍裡

\begin{equation} p_{i1} \vee p_{i2} \vee \cdots \vee p_{im} \end{equation}

代表鴿子 $i$ 號,要不住在一號鴿舍( $p_{i1}$ )、或是二號鴿舍( $p_{i2}$ )、…、或是 $m$ 號鴿舍( $p_{im}$ ),然後總共有 $n$ 隻鴿子。總之,給定一隻鴿子 $i$ ,牠一定住在共 $m$ 個鴿舍裡任意一個鴿舍裡(Given a pigeon $i$, there is exactly one hole $j$ for which $p_{i,j}$ is true.)。

for i in range(1, n+1):
    for j in range(1, m+1):
        print(m*(i-1)+j, end=' ')
    print("0")

一個鴿舍只會有一隻鴿子

This formula says that at most one pigeon lives in hole $k$.

代表對於第 $k$ 號鴿舍,最多只會有一隻鴿子。(Given a hole $j$, there is at most one pigeon $i$ for which $p_{ij}$ is true. )。所以很明顯的,當鴿子數量比鴿舍數量多($n>m$)的時候,SAT 無解。

\begin{equation} \bigwedge_{1\leq i < j \leq n} \neg p_{ik} \vee \neg p_{jk}\\ = (\neg p_{1k} \vee \neg p_{2k})\wedge(\neg p_{2k} \vee \neg p_{3k})\wedge\cdots\wedge(\neg p_{(n-1)k} \vee \neg p_{nk}) \end{equation}

for j in range(1, m+1):
    for i in range(1, m+1):
        for k in range(i+1, n+1):
            print(-(m*(i-1)+j), -(m*(k-1)+j), "0")

最後再把全部的 clause 用 $\wedge$ 串在一起,得到一個 boolean function,在匯出成 .cnf 檔。

Attachment

import sys

print("CAUTION : number of pigeons(n) and number of holes(m) can't be smaller than 0")

while(1):
    n = int(input("Enter the number of pigeons(n):"))
    m = int(input("Enter the number of holes(m):"))
    if (m*n > 0):
        break
    else:
        print("number of pigeons(n) or number of holes(m) can't be smaller than 0")
        print("Please retry.")
        continue

variable = n*m
clause = 0
finseq = []

for i in range(1, n+1):
    for j in range(1, m+1):
        continue
    clause = clause + 1
    
for j in range(1, m+1):
    for i in range(1, m+1):
        for k in range(i+1, n+1):
            clause = clause + 1

# PRINT IN COMMAND LINE

print("c")
print("c number of pigeons(n):", n, ",number of holes(m):", m)
print("c")
print("p cnf", variable, clause)

for i in range(1, n+1):
    tmp = []
    for j in range(1, m+1):
        print(m*(i-1)+j, end=' ')
        tmp.append(str(m*(i-1)+j)+" ")
    print("0")
    tmp.append("0")
    finseq.append(tmp)

for j in range(1, m+1):
    for i in range(1, m+1):
        for k in range(i+1, n+1):
            finseq.append(str(-(m*(i-1)+j)) + " " + str(-(m*(k-1)+j)) + " 0")
            print(-(m*(i-1)+j), -(m*(k-1)+j), "0")

# OUTPUT .CNF FILE

outputfilename = str(n) + "_pigeons_in_"+ str(m) +"_holes.cnf"
file = open(outputfilename, "w")

file.writelines("c\n")
file.writelines("c number of pigeons(n): " + str(n) + " ,number of holes(m): " + str(m) + "\n")
file.writelines("c\n")
file.writelines("p cnf " + str(variable) + " " + str(clause) + "\n")
for index in range(len(finseq)):
    file.writelines(finseq[index])
    file.writelines("\n")
file.close()