Modified SAT

The Boolean satisfiability problem (SAT) asks, given a Boolean formula in conjunctive normal form, whether there is an assignment of true or false to its variables that makes the whole formula true.

In conjunctive normal form, the formula has a specific shape. The only logical operations used are AND, OR, and negation, written $\wedge$, $\vee$, and $\neg$. A formula is the AND of several parts called clauses, $C_1, \dots, C_m$. So a formula $\phi$ has the form

$\phi = C_1 \wedge \cdots \wedge C_m.$

Each clause also has a specific shape. A clause is the OR of literals, which are variables or negations of variables, enclosed in parentheses. So $(x_1 \vee \neg x_2)$ is a valid clause, while $(x_1 \wedge \neg x_2)$ is not, because it uses AND. A complete example formula is

$\phi = (x_1 \vee x_2 \vee x_3) \wedge (\neg x_1) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (x_2 \vee \neg x_3).$

A variation of SAT is k-SAT, where each clause has at most $k$ literals. The formula above is a 3-SAT instance but not a 2-SAT instance. In all these problems, for a formula to be true every clause must be true, so at least one literal (of the form $x_i$ or $\neg x_i$) in each clause must be true.

An assignment is a way of setting the variables to true or false. This problem concerns a variation of 3-SAT in which a valid assignment must have exactly 1 or exactly 3 true literals in each clause. Given a formula, your task is to decide whether a valid assignment exists under this extra restriction. If a valid assignment exists, you must print the lexicographically largest one. Lexicographic order is defined as follows: given two different assignments, compare them at the lowest-indexed variable where they differ; the larger assignment is the one that sets that variable to true.

The first line contains two integers $M$ and $N$ ($1 \le M, N \le 2000$), the number of clauses and variables. Then $M$ lines follow, each describing one clause (see the example for the format). Consecutive clauses are separated by the string “ and”. Each clause contains at most 3 literals. Variables are written as “x” followed by a number between 1 and $N$. There are no two consecutive spaces, and no space at the end of a line.

The first example describes the formula $\phi$ above.

Print one line with $N$ characters for the lexicographically largest valid assignment, or impossible if no valid assignment exists. The $i$-th character is T if variable $i$ is true in the assignment and F otherwise.