Pattern matching problem with Prolog

EDIT: See my answer below for why I am a fool. There is still a riddle in this that I would love to have answered though.

I've been stuck on this for far too long. I'm trying to print out a sudoku solution in a nice looking grid.

I think I'm running into problems because I don't understand some key part of how pattern matching works in Prolog.

Without further ado, my code:

prettier_print([]).
prettier_print([Puzzle]) :- prettier_print(0, [Puzzle]).

prettier_print(0, Puzzle) :- 
    writeln('┌───────┬───────┬───────┐'), 
    prettier_print(1, Puzzle).
prettier_print(4, Puzzle) :- 
    writeln('│───────┼───────┼───────│'), 
    prettier_print(5, Puzzle).
prettier_print(8, Puzzle) :- 
    writeln('│───────┼───────┼───────│'), 
    prettier_print(9, Puzzle).
prettier_print(12, []) :- 
    writeln('└───────┴───────┴───────┘').

prettier_print(N, [Col1, Col2, Col3, Col4, Col5, Col6, Col7, Col8, Col9 | Puzzle]) :- 
    member(N, [1,2,3,5,6,7,9,10,11]),  % tried this when the line below did not work
    % N =\= 0, N =\= 4, N =\= 8, N =\= 13,

    format('│ ~d ~d ~d │ ~d ~d ~d │ ~d ~d ~d │~n', [Col1, Col2, Col3, Col4, Col5, Col6, Col7, Col8, Col9]), 
    succ开发者_JAVA技巧(N, N1),
    prettier_print(N1, Puzzle).

Here is the call:

prettier_print(0, [1,2,3,4,5,6,7,8,9, 
                   2,2,3,4,5,6,7,8,9, 
                   3,2,3,4,5,6,7,8,9, 
                   4,2,3,4,5,6,7,8,9, 
                   5,2,3,4,5,6,7,8,9, 
                   6,2,3,4,5,6,7,8,9,
                   7,2,3,4,5,6,7,8,9,
                   8,2,3,4,5,6,7,8,9,
                   9,2,3,4,5,6,7,8,9]).

And here is the output:

┌───────┬───────┬───────┐
│ 1 2 3 │ 4 5 6 │ 7 8 9 │
│ 2 2 3 │ 4 5 6 │ 7 8 9 │
│ 3 2 3 │ 4 5 6 │ 7 8 9 │
│───────┼───────┼───────│
│ 4 2 3 │ 4 5 6 │ 7 8 9 │
│ 5 2 3 │ 4 5 6 │ 7 8 9 │
│ 6 2 3 │ 4 5 6 │ 7 8 9 │
│───────┼───────┼───────│
│ 7 2 3 │ 4 5 6 │ 7 8 9 │
│ 8 2 3 │ 4 5 6 │ 7 8 9 │
│ 9 2 3 │ 4 5 6 │ 7 8 9 │
└───────┴───────┴───────┘
true ;
false.

The problem is it doesn't JUST return with true, I have to press ;, and then it returns false. This in turn means that my prettier_print/1 rule doesn't work properly.

I think I know enough to figure out that this means:

Prolog is backtracking and trying another interpretation of my rules (seeing if there is anything else it can unify with, if I'm understanding my terms correctly). This finds one other thing to unify with that, but that fails immediately. Is that right?

I want there to be only one possible interpretation. How can I fix my function to mean that?

Thank you for any help, this has me feeling like such a fool!

---

For one way to see this, try SWI-Prolog's graphical tracer:

?- gtrace, your_goal.

The tracer will show you where choicepoints are created, introducing non-determinism. On backtracking (for example, when you press SPACE or ";" on the toplevel), remaining alternative clauses will be considered.

---

It is "returning" true, then false, because you are forcing it to backtrack with ;. Since there's only one solution, backtracking fails.

This behavior only occurs in interactive Prolog interpreters; it you were to compile the program or run it in a non-interactive interpreter, it would just print the result and not "return" anything. This is somewhat similar to the behavior of, e.g., the Python interpreter

>>> 'foo'
'foo'

which echoes the value of the last expression entered, but only in interactive mode. A script wouldn't print anything unless you put in print statements.

If you don't want to see the false message then either don't backtrack, i.e. press Enter instead of ;, or use the metapredicate once/1:

?- member(X,[1,2,3]).
X = 1 ;
X = 2 .    % ENTER pressed here

?- once(member(X,[1,2,3])).
X = 1.

?- 

but don't just do that anywhere in a program, as it changes the program's semantics.

---

The reason why it is returning true and then false upon backtracking is that you are leaving choicepoints in your clauses. Your applications flow will only execute one clause of prettier_print/2, but the prolog interpreter does not know that in advance, so it leaves a choicepoint and then, upon backtracking, will try to see if any of the remaining clauses of prettier_print/2 will succeed.

You can "cut" backtracking, commiting to one choice by using the cut (!):

prettier_print([]).
prettier_print([Puzzle]) :- prettier_print(0, [Puzzle]).

prettier_print(0, Puzzle) :-
    writeln('┌───────┬───────┬───────┐'),
    !,
    prettier_print(1, Puzzle).
prettier_print(4, Puzzle) :-
    writeln('│───────┼───────┼───────│'),
    !,
    prettier_print(5, Puzzle).
prettier_print(8, Puzzle) :-
    writeln('│───────┼───────┼───────│'),
    !,
    prettier_print(9, Puzzle).
prettier_print(12, []) :-
    writeln('└───────┴───────┴───────┘'),
    !.
prettier_print(N, [Col1, Col2, Col3, Col4, Col5, Col6, Col7, Col8, Col9 | Puzzle]) :-
    member(N, [1,2,3,5,6,7,9,10,11]),  % tried this when the line below did not work

    format('│ ~d ~d ~d │ ~d ~d ~d │ ~d ~d ~d │~n', [Col1, Col2, Col3, Col4, Col5, Col6, Col7, Col8, Col9]),
    succ(N, N1),
    prettier_print(N1, Puzzle),
    !.

You may, as well, rewrite your solution so that you leave no choicepoints by using some other predicates instead of different clauses for prettier_print. This way you would not need to use the cut:

prettier_print(Puzzle) :-
  Puzzle \= [] ->
  (
    print_head,
    print_rows(Puzzle, NRows1),
    print_line,
    print_rows(Puzzle, NRows1),
    print_line,
    print_rows(Puzzle, NRows1),
    print_end
  ).

print_rows(Rows, NRows):-
  print_row(Rows, Rows1),
  print_row(Rows1, Rows2),
  print_row(Rows2, NRows).

print_head:-
    writeln('┌───────┬───────┬───────┐').

print_line:-
    writeln('│───────┼───────┼───────│').

print_end:-
    writeln('└───────┴───────┴───────┘').

print_row([Col1, Col2, Col3, Col4, Col5, Col6, Col7, Col8, Col9 | NRows], NRows) :-
    format('│ ~d ~d ~d │ ~d ~d ~d │ ~d ~d ~d │~n', [Col1, Col2, Col3, Col4, Col5, Col6, Col7, Col8, Col9]).

---

Augh, nevermind, I'm an idiot!

I had pinpointed something that wasn't a problem in the first place. Changing prettier_print/1 to this:

prettier_print([]).
prettier_print(Puzzle) :- prettier_print(0, Puzzle).

Makes it work fine.

I would still like to understand why it was returning true and then false though. If someone can answer that I'll mark their answer accepted.