Suppose we have two Boolean vectors, $x$ and $y$, of length $n$. How can I encode $x<_{\text{lex}}y$ into a CNF?
The only Boolean formula I can think of is $$(\neg x_0\land y_0)\lor\bigvee_{i=1}^{n-1}\left(\bigwedge_{j=0}^{i-1}(x_j=y_j)\land(\neg x_i\land y_i)\right)$$
but I cannot think of a way to make a similar CNF.
Thanks for any suggestions.
