Llaisdy

Futoshiki is a logic/number puzzle. Each row and column must contain all the numbers 1-9 (or whatever the size of the grid); the greater-than signs between some cells dictate that the number in one cell should be greater than its neighbour.

Here’s a question and solution from futoshiki.org:

This can be very simply implemented in clingo. Encoding the rules like this:

number(1..n).

cell(R, C) :- number(R), number(C).

% each cell has one number
1 { cell_has_number(R, C, N) : number(N) } 1 :- cell(R, C).

% same numbers may not share row or column
:- cell_has_number(R, C1, N), cell_has_number(R, C2, N), C1 != C2.
:- cell_has_number(R1, C, N), cell_has_number(R2, C, N), R1 != R2.

% greater than constraint
A > B :- greater_than(R1,C1, R2,C2),
         cell_has_number(R1,C1, A),
         cell_has_number(R2,C2, B).

#show cell_has_number/3.

Encode for example the question grid above like this:

#const n = 4.
cell_has_number(4,4, 2).
greater_than(1,2, 1,1).
greater_than(1,2, 1,3).
greater_than(3,3, 2,3).
greater_than(3,1, 4,1).
greater_than(4,2, 4,3).

Run like this (output tidied for readability):

$ clingo futoshiki.lp futoshiki-grid4.lp 0
clingo version 5.5.0
Reading from futoshiki.lp ...
Solving...
Answer: 1

cell_has_number(1,1,2)
  cell_has_number(1,2,3)
    cell_has_number(1,3,1)
      cell_has_number(1,4,4)

cell_has_number(2,1,4)
  cell_has_number(2,2,1)
    cell_has_number(2,3,2)
      cell_has_number(2,4,3)

cell_has_number(3,1,3)
  cell_has_number(3,2,2)
    cell_has_number(3,3,4)
      cell_has_number(3,4,1)

cell_has_number(4,1,1)
  cell_has_number(4,2,4)
    cell_has_number(4,3,3)
      cell_has_number(4,4,2)

SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.003s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.003s