My understanding of a logic is that it can be expressed statically and generally by limited number of math equations. For your example, it can be like this roughly.
exist(1,p1) and exist(2,p2) and exist(3,p3) and exist(4,p4) and exist(5,p5) and exist(6,p6) and exist(7,p7) and exist(8,p8) and exist(9,p9) = true where pi belongs to [1,9] and no two pi are the same.
From that, I can get p9=9 and exist(9,p9) = true
You can express the same for any rules that the explainer gets. The difference is that you don't know it or you don't know which one to apply from a vast number of rules until you try it.
Of course, expressing it and solving it is different. We can express any sudoku with something similiar to above. But solving it is another story. I don't remember anyone has tried to solve sudoku using old AI language like prolog, it will be sort of trial and error.
I lost interest in sudoku 6 years ago because it seemed to me there was no clear logical way to solve other than T&E. I did remember one of the forum discussed using logic expression to present it, someone even defined a set of equations and some systematic ways of applying them. But things may have changed and I would be happy to see there is a true one now.
Thanks a lot for posting the latest development.
