I am currently working on the queens problem defined as satisfiability problem. In the book I am following there is no explicit explanation how the upper bound is found (Q4 and Q5) to perform the check along the diagonals. Could anyone explain where min(i-1, n-j and min(n-i,n-j) are coming from?
Here, i is row, j is column.
I have done a research on this topic, however I couldn't find any answer to my question.
The book is Discrete Mathematics and its Applications, Kenneth H.Rosen, p.34access
Considering first Q5, i and j represent the row and column of the queen under consideration, the gist of the disjunction is to say that either there is not a queen at (i,j) or there is no queen at any other position on the diagonal direction currently under consideration.
The thing to note is it only calculates this for the part of the diagonal 'above' the queen (for efficiency). For example, taking the search at a certain point in the middle looks like:
thus we can see min(i-1,n-j) is the number of squares along the diagonal until you hit the edge of the board; i.e. the smaller of 'number of squares to the left' and 'number of sqaures above'. The other case is similar.
I have coded up the search, if you want to look yourself Rust Playground