Prolog infinity loop

Question

my code is the following,this code is a code for Sudoku solving but just for the row and column the first run of div2 check if the raw are all different then after transposing the second run of div2 should check if the column are all different.

:- use_module(library(clpfd)).  

len(P):-  
    div2(P),  
    write("\n 1P2:   "),  
    write(P),  
    transpose(P,X),  
    div2(X),  
    write("\n 1X:   "),  
    write(X).  

div2([H|T]) :-  
    H ins 1..9,  
    all_distinct(H),  
    label(H),  
    div2(T).  
div2([]).

why does it stuck in infinity loop ? when testing with this example it does repeat it self into an infinity loop where it should stop after the first run with X.

      len([
            [_,_,_,_,_,4,3,_,7],
            [7,6,_,1,5,_,_,_,9],
            [_,5,_,_,_,_,_,_,_],
            [6,_,5,_,_,8,7,_,_],
            [9,_,_,_,_,_,_,_,4],
            [_,_,3,2,_,_,1,_,5],
            [_,_,_,_,_,_,_,6,_],
            [5,_,_,_,3,1,_,2,8],
            [1,_,9,4,_,_,_,_,_]]).

Answer 1

Its not an "infinity loop", just a REALLY long one.

Suppose that div2(P) finds a proposed solution, which div2(X) then determines is not a solution. div2(P) will roll back & generate another solution by coming up with a new labelling for the last row only, at least until it has exhausted all ways to label the last row, then get a new labelling for the second-to-last-row, then run through all of the possibilities for the last row again. Roll that out through all 9 rows, and you have a LOT of combinations to go through, most of which look VERY similar.

Answer 2

@Scott's answer is right, your program actually does find all solutions. But it seems way too long for us to wait.

Instead, remove the label/1 goal, which is the source of enumerating those solutions and add it at the end!

latin_(P,Vs) :-
    div2(P),
    transpose(P,X),
    div2(X),
    append(P,Vs).

 latin(P) :-
    latin_(P, Vs),
    labeling([], Vs).

The idea in constraint programming with finite domains is to delay actual enumeration (labeling) to a later point. In this manner, labeling can take into account all of the existing constraints. The easiest way to ensure that you are following this approach is to split your predicate into two parts. The actual core-relation (latin_/2) and the complete relation (latin/1). Often, it is possible to observer termination of the core-relation while this would be very costly for the complete relation.