```///////////////////////////////////////////////////////////////////////////////
//
// Nine Card Puzzle  http://nifty.stanford.edu/2003/backtracking/
//
// Stephen Weiss
// Computer Science
// University of North Carolina at Chapel Hill
// CB# 3175, Sitterson Hall
// Chapel Hill, NC 27599-3175
//
// Arrange the nine squares (depicted below), so that the edges that touch
// There are 95,126,814,720 ways to arrange the squares (9!*(4**9)) and four
// solutions  (actually only one solution with four orientations).
//
// +------++------++------+
// |  -4  ||  -2  ||  -3  |
// | 2   1||-2   4|| 4   1|
// |  -3  ||   3  ||  -2  |
// +------++------++------+
// +------++------++------+
// |   3  ||   2  ||  -4  |
// |-4   2||-3  -1||-2   1|
// |  -1  ||   4  ||   3  |
// +------++------++------+
// +------++------++------+
// |  -3  ||  -1  ||  -2  |
// | 1  -2|| 3  -4||-1   1|
// |   2  ||   2  ||   2  |
// +------++------++------+

// There are other sets of squares possible, these can be also found at
// the above mentioned web address. Here we solve the first three sets.
// It is rather trivial to modify this program to solve the additional sets.
//
// To solve the puzzle using the first set of squares, issue the query
//
//     all NiftySquares(Pieces1)
//
// This will find all four solutions, which will be displayed in an easy
// to verify format, such as:
//
// +------++------++------+
// |   2  ||  -3  ||  -4  |
// | 3 D-1|| 1 G-2|| 2 A 1|
// |  -4  ||   2  ||  -3  |
// +------++------++------+
// +------++------++------+
// |   4  ||  -2  ||   3  |
// |-2 C-3|| 3 F-4|| 4 B-2|
// |   1  ||   1  ||  -2  |
// +------++------++------+
// +------++------++------+
// |  -1  ||  -1  ||   2  |
// | 2 I-2|| 2 E 4||-4 H 3|
// |   1  ||  -3  ||  -1  |
// +------++------++------+
//
// Note we added a letter for each square, so the square can be easily
// identified. This also makes it possible to visually confirm that indeed
// each square was used exactly once.
//
// To solve the puzzle using the second set of squares, issue the query
//
//     all NiftySquares(Pieces2)
//
// This set of squares will have 24 solutions.
//
// To solve the puzzle using the third set of squares, issue the query
//
//     all NiftySquares(Pieces3)
//
// This set of squares will have 32 solutions.
//
// Each set took less than one second to solve using an AMD Athlon1600+.
//
///////////////////////////////////////////////////////////////////////////////

Square = (up:I,right:I,down:I,left:I,letter:S)
Board = [0..8]->Square
AllPieces = [0..8]->[0..3]->Square // 9 squares each with 4 orientations

// Given the squares depicted above, create an array of arrays containing
// all the squares, each with all possible rotations. The order or direction
// of rotations is irrelevant. Here we simply rotate each square clockwise
// by 90 degrees.

Pieces1 :< AllPieces =
[  { no rotation}   { 90 degrees}      { 180 degrees}     { 270 degrees}
[(-4, 1,-3, 2,' A'),( 2,-4, 1,-3,' A'),(-3, 2,-4, 1,' A'),( 1,-3, 2,-4,' A')],
[(-2, 4, 3,-2,' B'),(-2,-2, 4, 3,' B'),( 3,-2,-2, 4,' B'),( 4, 3,-2,-2,' B')],
[(-3, 1,-2, 4,' C'),( 4,-3, 1,-2,' C'),(-2, 4,-3, 1,' C'),( 1,-2, 4,-3,' C')],
[( 3, 2,-1,-4,' D'),(-4, 3, 2,-1,' D'),(-1,-4, 3, 2,' D'),( 2,-1,-4, 3,' D')],
[( 2,-1, 4,-3,' E'),(-3, 2,-1, 4,' E'),( 4,-3, 2,-1,' E'),(-1, 4,-3, 2,' E')],
[(-4, 1, 3,-2,' F'),(-2,-4, 1, 3,' F'),( 3,-2,-4, 1,' F'),( 1, 3,-2,-4,' F')],
[(-3,-2, 2, 1,' G'),( 1,-3,-2, 2,' G'),( 2, 1,-3,-2,' G'),(-2, 2, 1,-3,' G')],
[(-1,-4, 2, 3,' H'),( 3,-1,-4, 2,' H'),( 2, 3,-1,-4,' H'),(-4, 2, 3,-1,' H')],
[(-2, 1, 2,-1,' I'),(-1,-2, 1, 2,' I'),( 2,-1,-2, 1,' I'),( 1, 2,-1,-2,' I')]
]

Pieces2 :< AllPieces =
[  { no rotation}   { 90 degrees}      { 180 degrees}     { 270 degrees}
[( 1, 2,-3,-4,' A'),(-4, 1, 2,-3,' A'),(-3,-4, 1, 2,' A'),( 2,-3,-4, 1,' A')],
[( 1,-4, 3,-2,' B'),(-2, 1,-4, 3,' B'),( 3,-2, 1,-4,' B'),(-4, 3,-2, 1,' B')],
[( 1,-3,-2, 4,' C'),( 4, 1,-3,-2,' C'),(-2, 4, 1,-3,' C'),(-3,-2, 4, 1,' C')],
[( 3, 2,-4,-1,' D'),(-1, 3, 2,-4,' D'),(-4,-1, 3, 2,' D'),( 2,-4,-1, 3,' D')],
[(-3, 1, 4,-2,' E'),(-2,-3, 1, 4,' E'),( 4,-2,-3, 1,' E'),( 1, 4,-2,-3,' E')],
[( 2, 4,-3,-1,' F'),(-1, 2, 4,-3,' F'),(-3,-1, 2, 4,' F'),( 4,-3,-1, 2,' F')],
[( 4,-1,-2, 3,' G'),( 3, 4,-1,-2,' G'),(-2, 3, 4,-1,' G'),(-1,-2, 3, 4,' G')],
[(-4,-2, 3, 1,' H'),( 1,-4,-2, 3,' H'),( 3, 1,-4,-2,' H'),(-2, 3, 1,-4,' H')],
[( 3,-1,-4, 2,' I'),( 2, 3,-1,-4,' I'),(-4, 2, 3,-1,' I'),(-1,-4, 2, 3,' I')]
]

Pieces3 :< AllPieces =
[  { no rotation}   { 90 degrees}      { 180 degrees}     { 270 degrees}
[( 1, 2,-3,-4,' A'),(-4, 1, 2,-3,' A'),(-3,-4, 1, 2,' A'),( 2,-3,-4, 1,' A')],
[( 1,-4, 3,-2,' B'),(-2, 1,-4, 3,' B'),( 3,-2, 1,-4,' B'),(-4, 3,-2, 1,' B')],
[(-3, 1,-2, 4,' C'),( 4,-3, 1,-2,' C'),(-2, 4,-3, 1,' C'),( 1,-2, 4,-3,' C')],
[( 3, 2,-4,-1,' D'),(-1, 3, 2,-4,' D'),(-4,-1, 3, 2,' D'),( 2,-4,-1, 3,' D')],
[(-3, 1, 4,-2,' E'),(-2,-3, 1, 4,' E'),( 4,-2,-3, 1,' E'),( 1, 4,-2,-3,' E')],
[( 2, 4,-3,-1,' F'),(-1, 2, 4,-3,' F'),(-3,-1, 2, 4,' F'),( 4,-3,-1, 2,' F')],
[( 4,-1,-2, 3,' G'),( 3, 4,-1,-2,' G'),(-2, 3, 4,-1,' G'),(-1,-2, 3, 4,' G')],
[(-4,-2, 3, 1,' H'),( 1,-4,-2, 3,' H'),( 3, 1,-4,-2,' H'),(-2, 3, 1,-4,' H')],
[( 3,-4,-1, 2,' I'),( 2, 3,-4,-1,' I'),(-1, 2, 3,-4,' I'),(-4,-1, 2, 3,' I')]
]

local Used = [0..8]->I // Type to keep track of used squares

///////////////////////////////////////////////////////////////////////////////
//
// Main predicate to solve the Nine Cards Puzzle
//
///////////////////////////////////////////////////////////////////////////////
pred NiftySquares(squares:<AllPieces) iff
board::Board &

// We keep track of used squares in the array "used".
// We initialize the map of used squares to 0 (no square used)
used :.Used & Dupl(9,0,used) &

// Solve the puzzle by placing all nine squares
PlaceSquares(board,squares,used,0) &

// Display each solution
PrintFormattedSolutions(board)

///////////////////////////////////////////////////////////////////////////////
//
// Place all nine squares on the board.
//
pred PlaceSquares(board::Board,squares:<AllPieces,used:.Used,i:<I) iff
if i < 9 then
PlaceOneSquare(board,squares,used,i) &
PlaceSquares(board,squares,used,i+1)
end

///////////////////////////////////////////////////////////////////////////////
//
// Place one (sofar unused) square on the board. The code will automatically
// backtrack through all unused squares and available rotations until we
// succeed. Afterwards mark the successfully placed square as used.
//
local pred PlaceOneSquare(board::Board,squares:<AllPieces,used:.Used,i:<I) iff
p::I[0..8] & used(p) = 0 &  // get an unused square index
piece = squares(p) &        // get an unused square
rot::I[0..3] &              // each square can have four rotations

// place the new square on the board
board(i) = piece(rot) &

// easier to use rows and columns...
col = i mod 3 & row = i /3 &

// specify constraints:
// left+right edges add up to zero
// bottom+top edges add up to zero

if col > 0 then
board(row*3+col-1).right + board(row*3+col).left = 0
end &
if row > 0 then
board((row-1)*3+col).down + board(row*3+col).up = 0
end &

// finally, mark the square as used so we don't use the same square again
used(p) := 1

///////////////////////////////////////////////////////////////////////////////
//
// Print each solution in an user friendly manner.
//
local proc PrintFormattedSolutions(board:<Board) iff
Print('\n\n') &
PrintNiftySquares(board,0) &    // Print row 0
PrintNiftySquares(board,1) &    // Print row 1
PrintNiftySquares(board,2)      // Print row 2

///////////////////////////////////////////////////////////////////////////////
//
// Print one row (three squares at a time) to get an easy to read format.
//
local proc PrintNiftySquares(a:<Board,row:<I) iff
Print('+------++------++------+\n') &
Print('|  ') & PrintNum(a(row*3+0).up) & Print('  ||  ') &
PrintNum(a(row*3+1).up) & Print('  ||  ') &
PrintNum(a(row*3+2).up) & Print('  |\n' ) &
Print('|')   & PrintNum(a(row*3+0).left) & Print(a(row*3+0).letter) & PrintNum(a(row*3+0).right) & Print('||') &
PrintNum(a(row*3+1).left) & Print(a(row*3+1).letter) & PrintNum(a(row*3+1).right) & Print('||') &
PrintNum(a(row*3+2).left) & Print(a(row*3+2).letter) & PrintNum(a(row*3+2).right) & Print('|\n') &
Print('|  ') & PrintNum(a(row*3+0).down) & Print('  ||  ') &
PrintNum(a(row*3+1).down) & Print('  ||  ') &
PrintNum(a(row*3+2).down) & Print('  |\n' ) &
Print('+------++------++------+\n')

///////////////////////////////////////////////////////////////////////////////
//
// Print each number as two characters. Negative numbers will print a minus
// sign '-' automatically, for positive numbers print a leading space character.
//
local proc PrintNum(a:<I) iff
if a >= 0 then Print(' ') end & Print(a)

```