:- use_module(library(clpfd)). :- use_module(library(lists)). domain(Vars, Lower, Upper) :- Vars ins Lower..Upper. /* Simple Minesweeper puzzle MS0 2 _ 4 _ _ _ _ _ _ 3 _ 1 */ /* CLPFD representation Variables: Assign a variable to each cell in which there can be a mine: 2 A 4 B C D E F G 3 H 1 Domains: A in 0..1, etc, A = 0 means no mine, A = 1 means mine Constraints: 2 in the top left corner means exactly 2 of A, C, D are mines: A+C+D #= 2. 4 in row 1 means exactly 4 of A, B, D, E, F are mines: A+B+D+E+F#=4, etc. */ % List is a solution of puzzle MS0 ms00(List) :- List=[A,B,C,D,E,F,G,H], domain(List, 0, 1), A+C+D#=2, A+B+D+E+F#=4, C+D+E+G+H#=3, E+F+H#=1. /* | ?- ms00(L). L = [_A,_B,_C,_D,_E,_F,_G,_H], _A in 0..1, _B in 0..1, _C in 0..1, _D in 0..1, _E in 0..1, _F in 0..1, _G in 0..1, _H in 0..1 ? ; no | ?- ms00(L), labeling([], L). L = [1,1,0,1,1,0,1,0] ? ; no */ % Labeling the Kth variable of List binds all variables % Recall: ground(L) means there are no unbound vars in L run00(List, K) :- ms00(List), nth1(K, List, V), indomain(V), ground(List). /* | ?- run00(L, K). L = [1,1,0,1,1,0,1,0], K = 5 ? ; L = [1,1,0,1,1,0,1,0], K = 6 ? ; no */ % A variant which solves the puzzle without labeling ms01(List, EF) :- List=[A,B,C,D,E,F,G,H], domain(List,0,1), E+F #= EF, A+C+D #= 2, A+B+D+EF #= 4, C+D+E+G+H #= 3, EF+H #= 1. /* | ?- ms01(L, _). L = [1,1,0,1,1,0,1,0] ? ; no */ /* Edited script for tracing the minesweeper problem using library(fdbg) -- SICStus only. | ?- use_module(library(fdbg)). | ?- fdbg_on, L=[A,B,C,D,E,F,G,H], fdbg_assign_name(A, 'A'), ..., fdbg_assign_name(EF, 'EF'), ms01(L, EF). A + B + D + EF #=4 A = 0..1, B = 0..1, D = 0..1, EF = 0..2 -> 1..2 H + EF #=1 H = 0..1 -> {0}, EF = 1..2 -> {1} Constraint exited. A + B + D + EF #=4 A = 0..1 -> {1}, B = 0..1 -> {1}, D = 0..1 -> {1}, EF = {1} Constraint exited. A + C + D #=2 A = {1}, C = 0..1 -> {0}, D = {1} Constraint exited. C + D + E + G + H #=3 C = {0}, D = {1}, E = 0..1 -> {1}, G = 0..1 -> {1}, H = {0} Constraint exited. E + F #= EF E = {1}, F = 0..1 -> {0}, EF = {1} Constraint exited. L = [1,1,0,1,1,0,1,0], EF = 1 ? */