/*
Langford's number problem with domain tracing in Picat.
See http://hakank.org/picat/langford.pi
Model created by Hakan Kjellerstrand, hakank@gmail.com
See also my Picat page: http://www.hakank.org/picat/
*/
import util.
import cp.
import trace_domains.
main => go.
go =>
K = 12,
printf("K: %d\n", K),
time2(langford(K, Solution, Position)),
trace_domains1d(Solution,solution,"Solution after solve"),
trace_domains1d(Position,position,"Position after solve"),
printf("Solution: %w\n", Solution),
printf("Position: %w\n", Position),
nl.
langford(K, Solution, Position) =>
if not ((K mod 4 == 0; K mod 4 == 3)) then
println("There is no solution for K unless K mod 4 == 0 or K mod 4 == 3"),
fail
end,
K2 = 2*K,
Position = new_list(K2),
Position :: 1..K2,
reset_trace_domains(solution),
reset_trace_domains(position),
trace_domains1d(Position,position,"Position Init"),
Solution = new_list(K2),
Solution :: 1..K,
trace_domains1d(Solution,solution,"Solution Init"),
% symmetry breaking:
Solution[1] #< Solution[K2],
trace_domains1d(Position,position,"Position after 1 #< 2"),
trace_domains1d(Solution,solution,"Solution after 1 #< 2"),
% all_different(Position),
all_distinct(Position),
trace_domains1d(Position,position,"Position after all_different"),
foreach(I in 1..K)
Position[K+I] #= Position[I] + I+1,
element(Position[I],Solution,I),
element(Position[K+I],Solution,I),
trace_domains1d(Position,position,"Position Loop I"=I),
trace_domains1d(Solution,solution,"Solution Loop I"=I)
end,
trace_domains1d(Position,position,"Position before solve"),
trace_domains1d(Solution,solution,"Solution before solve"),
Vars = Solution ++ Position,
solve([ff,updown], Vars).