Background
This is Post's lattice:
Credit: EmilJ
It denotes the lattice of all clones on a two-element set {0, 1}
, ordered by inclusion (from Wikipedia). That can be a bit of a mouthful so lets look at a concrete example. MP
(located near the top) is a set that contains all boolean circuits that can be made with and
and or
. DM
(a bit lower) is the set of all boolean circuits that can be made with the majority gate. The majority gate (maj
) takes three inputs and returns true iff at least two of the inputs are true. This is a hasse diagram ordered by inclusion, which means that since DM
is below M
and you can reach it by a sequence of nodes at decreasing heights, DM
is a (strict) subset of M
. This means that every circuit that can be made with maj
can be replicated using ∧
and ∨
.
I've colored the nodes according to the computational complexity of the boolean satisfiability problem restricted to that set of circuits. Green means O(1)
. This means that either the set is always satisfiable or it contains a finite amount of elements. Yellow is linear time. Red is NP-complete.
As you can see, \$T_0^\infty\$ is the smallest NP-complete set. It is generated by ↛
which is the negation of implication. In other words, it is the set of all formulas consisting of ↛
and brackets.
Task
Your task is to solve a instance of nonimplication-SAT. That is, you are given a boolean formula consisting of variables and the operator ↛
which has the following truth table:
a b a↛b
0 0 0
0 1 0
1 0 1
1 1 0
Your program has to decide whether there is an assignment to the variables which satisfies the formula. That is, the value of the formula is 1
.
Test cases
a↛a: UNSAT
a↛b: SAT
(a↛b)↛b: SAT
((a↛(c↛a))↛(b↛(a↛b)))↛(a↛(b↛c)): UNSAT
Rules
This is a decision problem so you should have two distinct output values for SAT and UNSAT. Use a reasonable input format. For example:
"(a↛(b↛c))↛(b↛a)"
[[0,[1,2]],[1,0]]
"↛↛a↛bc↛ba"
Make sure that the format you choose can handle an unlimited amount of variables. For strings just the letters a to z are not enough as there is only a finite amount of them.
Bonus points if your code runs in polynomial time :p