3xp-1: 3SAT

On this level puzzles will assume that you are willing to write small programs or scripts to help you out. If this is not the case, try the pp puzzle instead.

Problem Description

Consider 128 literals $l_1,...,l_{128}$ that can either be true or false. Let $f$ be a formula in conjunctive normal form whose $212$ clauses alternate between containing three literals $(l_i \lor l_j \lor l_k)$ or three negated literals $(\lnot l_i \lor \lnot l_j \lor \lnot l_k)$. Let the indices of literals appearing in this formula be given by the sequence $a_i$ counting from $1$ to $128$ in steps of $1$, then again in steps of $2,...,63$, ie. $a = (1,2,3,...,128,1,3,5,...,127,1,4,7,...)$. $f$ is then of the form

$$\begin{align} f(l) = &\quad (l_1 \lor l_2 \lor l_3) \land (\lnot l_4 \lor \lnot l_5 \lor \lnot l_6) \\ &\land \ldots \land (\lnot l_{124} \lor \lnot l_{125} \lor \lnot l_{126}) \land (l_{127} \lor l_{128} \lor l_1) \\ &\land \ldots \land (l_1 \lor l_{63} \lor l_{125}) \land (\lnot l_1 \lor \lnot l_{64} \lor \lnot l_{127}) \end{align}$$

Find a valid configuration for the $128$ literals that satisfies the formula $f(l)$.

Solution

To submit the solution to this puzzle join the Discord server and directly message _P the following text !solve 3xp-1 <l> where you have replaced <l> by a valid configuration that satisfies $f(l)$ in hex format (ie. one bit per literal, the first hex digit representing literals $l_1,l_2,l_3,l_4$ and so on).