405343: GYM101908 M Modifying SAT

The Boolean satisfiability problem (SAT) is to decide, given a Boolean formula in conjunctive normal form, if there is any assignment of values true or false to each variable so that the formula is true. In conjunctive normal form, the formula is given in a very specific format. Firstly, the only logical operations used are the "and", "or" and the negation, denoted by $$$\wedge$$$, $$$\vee$$$ and $$$\neg$$$, respectively. A formula is formed through operation "and" of different parts, denoted clauses, $$$C_1, \dots, C_m$$$. In this way, a formula will have the following format:

In addition, each of the clauses also has a specific format. In particular, each of the clauses is composed by the "or" of literals, which are variables or negations of variables surrounded by parenthesis. Thus $$$(x_1 \vee \neg x_2)$$$ is a valid clause, while $$$(x_1 \wedge \neg x_2)$$$ is not because of the operator "and". A complete example of formula would be:

A variation of SAT is known as $$$k$$$-SAT, where each clause has at most $$$k$$$ literals. The formula above would be an instance of the 3-SAT problem, but not 2-SAT. Note that, in all of these problems, for a formula to be true, each of the clauses must be true and, therefore, at least one of the literals (the form $$$x_i$$$ or $$$\neg x_i$$$) of each clause must be true.

An assignment is a way to set the variables as true or false. In this problem we are interested in a variation of the 3-SAT problem, in which a valid assignment must have exactly 1 or exactly 3 literals true in each clause. Given a formula, your task is to decide whether there is a valid allocation, taking into account such extra constraint. If there is a valid assignment, you must print the lexicographically largest one. The lexicographical order is defined as follows: given two different assignments, we can compare them by looking for the smaller variable index that differs on the two assignments; of the two assignments, the greater is the one that gives true value for this variable.

The first line of the input contains two integers $$$M$$$ and $$$N$$$ ($$$1 \leq M, N \leq 2000$$$), describing the number of clauses and variables, respectively. Then $$$M$$$ lines shall be provided, each describing a clause (see example for details of the format). Consecutive clauses are separated by the string and. Each clause contains at most 3 literals. The variables are denoted by x followed by a number between 1 and $$$N$$$. There will be no two consecutive spaces or spaces at the end of the lines. The first example describes the formula $$$\varphi$$$ defined right above.

Your program must print a single line containing $$$N$$$ characters corresponding to a valid assignment that is the lexicographically largest, or impossible if there is no valid assignment. The $$$i$$$-th character must be T if the variable is true on the assignment and F otherwise.

4 3
(x1 or x2 or x3) and
(not x1) and
(x1 or not x2 or x3) and
(x2 or not x3)

impossible

5 6
(not x1) and
(x1 or x2 or x4) and
(x1 or x3 or x5) and
(not x2 or x3 or x5) and
(x2 or x3 or not x4)

FTTFFT

1 1
(x1 or x1 or not x1)

F