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.



You must log in to answer this question.

Browse other questions tagged .