用Answer Set Programming解数独

搜索“ASP solver”可以得到若干个，clasp是其中一个http://www.cs.uni-potsdam.de/clasp/?page=main

有本教程叫A User's Guide to gringo, clasp, clingo, and iclingo，Google一下就可以下到

Answer Set Programming的优点在于，你只需要定义规则，求解的方法由ASP solver来解决，这是一种declarative language，和SQL同类

 看如下这个数独（http://www.sudoku.name/index-cn.php）：

首先描述facts(文件sudoku_fact.lp)：

row(1..9).
col(1..9).
value(1..9).
put(1,2,9).
put(1,4,7).
put(1,6,6).
put(1,7,1).

put(2,2,2).
put(2,3,5).
put(2,4,3).
put(2,8,6).
put(2,9,7).

put(3,3,6).
put(3,5,2).
put(3,8,8).

put(4,1,5).
put(4,6,9).
put(4,7,3).

put(5,1,7).
put(5,3,3).
put(5,5,4).
put(5,7,2).
put(5,9,8).

put(6,3,8).
put(6,5,3).
put(6,6,7).
put(6,9,6).

put(7,2,8).
put(7,5,5).
put(7,7,6).

put(8,1,4).
put(8,2,3).
put(8,6,8).
put(8,7,7).
put(8,8,2).

put(9,3,9).
put(9,4,1).
put(9,6,2).
put(9,8,3).

其中put(x,y,z)表示第x行第y列的值为z；row(1..9).表示row的取值为1到9，对col和value类似

然后描述规则（文件sudoku_enc.lp）：

%Default,%开头的是注释
#const n = 9.
%Generate
1 { put(X,Y,1..n) } 1 :- row(X),col(Y).
%Test
:- put(A,B,C), put(A,D,C), B != D.
:- put(A,B,C), put(D,B,C), A != D.
:- put(A,B,C), put(D,E,C), (A-1) #div 3 == (D-1) #div 3, (B-1) #div 3 == (E-1) #div 3, A != D, B != E.

去掉3行注释，再去掉定义n=9这个常量，实际只有4行，每一行都是一条规则(rule)

第1行表示：第X行第Y列只能放一个值——显然，每个空格只能填一个值。

{ put(X,Y,1..n) }是{ put(X,Y,1) , put(X,Y,2), ... , put(X,Y,n)}的简写，叫语法糖（syntax sugar），就是为了方便而存在的东西， 这个式子首尾的两个1分别表示{}中成立的文字(literal)的个数的下界和上界，这里上界和下界相同，表示只有一个文字成立。

":-"表示右边可以推出左边，即如果右边所有文字(literal)都为真，则左边必为真。":-"左边部分称为规则的头(head)，右边称为规则的体(body)，规则体之间的逗号可以看成“&&”，或者合取

row(X)表示X在fact所定义的0到9之间，col类似

第2行表示：同一行的不同位置不能放相同的数字

“:-”作为开头，即规则的头为空，后面跟的是需要排除的情况，也称为约束(constraint)

第3行表示：同一列的不同位置不能放相同的数字

第4行表示：同一个3×3的小九宫格的不同位置不能放相同的数字

#div表示整数除法，例如1 #div 3 = 0, 2 #div 3 = 0, 3 #div 3 = 1，就是C语言中的整数除法

所以第1个九宫格（行号-1）#div 3的结果是0，（列号-1）#div 3的结果也是0，这两个值组成数对(0,0)唯一标识了这个小九宫格，这是一个小技巧，使得我们这里的规则可以写得简洁到只需要一句话。

调用iclingo.exe来求解：iclingo.exe sudoku_fact.lp sudoku_enc.lp

最终结果是：

3  9  4  7  8  6  1  5  2
8  2  5  3  1  4  9  6  7
1  7  6  9  2  5  4  8  3
5  4  2  8  6  9  3  7  1
7  6  3  5  4  1  2  9  8
9  1  8  2  3  7  5  4  6
2  8  7  4  5  3  6  1  9
4  3  1  6  9  8  7  2  5
6  5  9  1  7  2  8  3  4

和标准答案一致

从iclingo的输出还可以知道，这是唯一解。

此外，为了格式化输出，这里写了一个格式化小程序format.cpp，一并贴上来

#include <stdio.h>
#include <iostream>
#include <string>
using namespace std;
int x[10][10];
int main(int argc, const char *argv[])
{
    int a, b, c;
    string s;
    //while (scanf("put(%d,%d,%d) ", &a, &b, &c) == 3) {
    while(cin >> s) {//detect 'put'
        if (s[0] == 'p') {
            x[s[4] - '0'][s[6] - '0'] = s[8] - '0';
        }
    }
    for (int i = 1; i < 10; i++) {
        for (int j = 1; j < 10; j++) {
            printf("%d  ", x[i][j]);
        }
        printf("\n");
    }
    return 0;
}

用的时候可以借助管道：iclingo.exe sudoku_fact.lp sudoku_enc.lp | format.exe