Proof that $N=49$ is impossible:
+-------+--- 1) +-------+ 2) +-------+ 3) +-------+
| 1 2 3 | X |(1)2 3 |*1 | 1 2 3 |(7) | 1 2 3 |(4)
| 4 5 6 | Y |(4)5 6 |*4 | 4 5 6 | 1 |(4)5 6 | 7
| 7 8 9 | Z |(7)8 9 |*7 |(7)8 9 | 4 | 7 8 9 | 1
+-------+--- +-------+ +-------+ +-------+
| A B C | D | A B C | D | A*B*C |*D | A*B*C |*D
The block on the first figure is to be taken as our "starting" one. Since there are no other numbers on the board, having them ordered makes no difference, for now. Now, there are 3 different ways to fill tiles XYZ with 1 4 and 7, but they all fail. Since:
Case 1: Obviously, there's 3 collisions.
Case 2: BCD must contain 237 on any order. However, 7 can't be on B or C because it collides with our original grid. And it can't be on D either, because it's on the same row as the recently added one.
Case 3: Similar to before, except with 4.
That means there's no way to have those 2 blocks (23X,56Y,89Z and 56Y,89Z,BCD) successfully.
Therefore, $N=49$ is impossible.
Remember that first-order logic has no idea what a 'digit' is, so you'll need to specify that:
$\forall x (x=1 \lor x=2 \lor x=3 \lor x=4 \lor x=5 \lor x=6 \lor x=7 \lor x=8 \lor x = 9)$
In fact, even that is not enough, since just because you have different symbols does not mean that they should denote different objects. So, you'll actually have to specify that these are all different, i.e. you need:
$1 \not = 2$, $1 \not = 3$, etc.
Even then, first-order has no idea that $1$ is 'next' to $2$, etc. ... but you'll need that knowledge to indicate the blocks .. or at least that $1$,$2$, and $3$ go together, and same for $4$, $5$, $6$, and for $7$, $8$, $9$
So, maybe have a two-place $b$ relation to indicate that:
$b_{1,2}$, $b_{2,3}$, $b_{4,5}$, $b_{5,6}$, $b_{7,8}$, $b_{8,9}$
and take its symmetric and transitive closure:
$\forall z_1 \forall z_2 (b_{z_1,z_2} \to b_{z_2,z_1})$
$\forall z_1 \forall z_2 \forall z_3 ((b_{z_1,z_2} \land b_{z_2,z_3})\to b_{z_1,z_3})$
And now you can specify that there cannot be two of the same digits in the same block:
$\forall x_1 \forall x_2 \forall y_1 \forall y_2 \forall v ((a_{x_1,y_1,v} \land \neg (x_1 = x_2 \land y_1 = y_2) \land b_{x_1,x_2} \land b_{y_1,y_2}) \to \neg a_{x_2,y_2,v})$
Oh, and finally, make sure to say that every square needs a digit!
$\forall x \forall y \exists v \ a_{x,y,v}$
Best Answer
The formula says "for every allowed value of the row $i$ and the value $n$, there is at least one column $j$ for which the $(i,j)$ location of the grid is filled with the value $n$".
The translation of Sudoko to propositional logic does not make the problem fundamentally easier. Any logic problem can be rewritten as a Sudoku, too, and solving either type of problem in general is computationally difficult (NP-complete).
No, the formula saying that is $\bigvee_{j=1}^{9}~p(1,j,1)$ which is the $i=1$,$n=1$ specialization of the first formula. The disjunction indexed by $j$ unpacks to "p(1,1,1) OR p(1,2,1) OR p(1,3,1) OR ... p(1,9,1)".