How to translate sudoku XV boards in CNF format?

Question

I'm trying to implement the logic for a Sudoku XV puzzle, that it's essentially a standard sudoku with the addition of X and V markers between some pairs of squares. X markers in adjacent pairs requires that the sum of the two values is 10. Similarly, the V marks requires that the sum of the values is equal to 5.

(Assume that $$ S_{xyz} $$ stands for [digit][row][column])

I've written the following CNF formulae that handle the logic of a standard Sudoku puzzle:

There is at least one number in each entry: $$ \bigwedge_{x=1}9\bigwedge_{y=1}9\bigwedge_{z=1}9S_{xyz} $$

Each number appears at most once in each row: $$ \bigwedge_{y=1}9\bigwedge_{z=1}9\bigwedge_{x=1}{8\bigwedge_{i=x+1}9}{(\lnot S}_{xyz\ }\vee\lnot S_{iyz\ }) $$

Each number appears at most once in each column: $$ \bigwedge_{x=1}9\bigwedge_{z=1}9\bigwedge_{y=1}{8\bigwedge_{i=x+1}9}{(\lnot S}_{xyz\ }\vee\lnot S_{xiz\ }) $$

Each number appears at most once in each 3x3 sub-grid: $$ \bigwedge_{z=1}9\bigwedge_{i=0}2\bigwedge_{j=0}{2\bigwedge_{x=1}2\bigwedge_{y+1}3\bigwedge_{k=x+1}3\bigwedge_{l=1,\ \ y \neq l}3}{(\lnot S}_{(3i+x)(3j+y)z\ }\vee\lnot S_{(3i+k)(3j+l)z\ }) $$

Unfortunately, I'm stuck, and I don't really know how I can express the logic for X and V markers, and most importantly how to invalidate squares that contain neither an X nor a V marker that have digits summing to 5 or 10.

Answer 1

I'm a new contributor so I can only add a comment in an answer post. This is a very general comment. The solving logic of a sudoku puzzle resides least in the visible digits (entries) than in the invisible candidates. The candidates state space can be represented by a 9x9x9x9 boolean matrix, the coordinates of which are (candidate, row, column, block). In that space the X and V logics can easily be expressed.