搜索“ASP solver”可以得到若干个，clasp是其中一个?page=main
有本教程叫A User’s Guide to gringo,clasp, clingo, and iclingo，Google一下就可以下到
Answer Set Programming的优点在于，你只需要定义规则，求解的方法由ASP solver来解决，这是一种declarative language，和SQL同类
看如下这个数独（）：
首先描述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.%Generate1 { 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.exesudoku_fact.lpsudoku_enc.lp
最终结果是：
3 9 4 7 8 6 1 5 28 2 5 3 1 4 9 6 71 7 6 9 2 5 4 8 35 4 2 8 6 9 3 7 17 6 3 5 4 1 2 9 89 1 8 2 3 7 5 4 62 8 7 4 5 3 6 1 94 3 1 6 9 8 7 2 56 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;(cin >> s) {(s[) {x[s[][s[] = s[;}}for (int i = 1; i < 10; i++) {for (int j = 1; j < 10; j++) {printf(, x[i][j]);}printf();}return 0;}
用的时候可以借助管道：iclingo.exesudoku_fact.lpsudoku_enc.lp | format.exe
不是每一次努力都有收获，但是，每一次收获都必须经过努力。
