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.
Take the aforementioned DNF formula, and negate it to obtain a CNF formula $\Phi(x, y)$ in polynomial-time. Note that the CNF formula $\Phi(x, y)$ evaluates to true on all input vectors $x, y$ such that $x \geq y$. Add the following additional clauses to $\Phi$ to ensure that $x \neq y$:
$$ (x_0 \lor y_0) \land (\neg x_0 \lor \neg y_0) \land \ldots $$
Now the formula is true for all inputs $x, y$ such that $x > y$. Finally, swap the $x$ and $y$ variables to obtain what you need.