Description. I have $m \in \mathbb N$ and three possible logical expressions, which I immediately presented in the most convenient notation:
- $X \to Y = \lnot X \lor Y$
- $X \to \lnot Y = \lnot X \lor \lnot Y$
- $X \lor Y$
Let's agree to call logical components $X$ or $Y$ just components. They can take any value from the set $\{X_1, X_2,\ldots,X_m\}$, where $X_i \in \{0, 1\}$.
The above logical expressions can be combined with each other using the conjunction. It is input expression. For example, for $m=3$ we can have an expression like this $(\lnot X_1 \lor X_2) \land (\lnot X_2 \lor \lnot X_3) \land (X_1 \lor X_3)$. But each boolean expression is optional. That is, there can be an expression of this kind $(\lnot X_1 \lor X_2) \land (X_1 \lor X_3)$
Problem. I have input expression which is described above. It is necessary to determine whether such a set $\{X_1, X_2,\ldots,X_m\}$ exists for any $m$ for which the input expression takes the value $1$.
For example, there is no answer for the input expression $(\lnot X_1 \lor X_3) \land (\lnot X_2 \lor X_1) \land (\lnot X_3 \lor \lnot X_1) \land (X_1 \lor X_2) = X_1 \land \lnot X_1 \neq 1$.
My idea. I use gluing for convert the input expression to disjunctive normal form. It works well. But I don't understand what to do next, because sometimes disjunctive normal form is more difficult than $X_1 \land \lnot X_1$. For example like here $(\lnot X_3 \lor X_2) \land (X_1 \lor X_2)$. It's not difficult to calculate this with your hands, but I need to program an algorithm.