Solve nonimplication-SAT

Question

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

Answer 1

Wolfram Language (Mathematica), 30 bytes

SatisfiableQ[#/.$->(#&&!#2&)]&

Try it online!

Takes input in the form $[$[a, $[b, c]], $[b, a]].

Answer 2

Charcoal, 57 bytes

Ｗ⁻⪪⁻⁻θ(¦)¦>υ⊞υ⌊ι⊙…⁰Ｘ²ＬυＵＶ⪫⟦(lambda ⪫λ=0,¦=0:θ)(⪫⮌↨ι²,¦)⟧ω

Try it online! Link is to verbose version of code. Accepts any valid Python identifier as a variable name and represents the nonimplication operator with the > character. Outputs a Charcoal boolean, i.e. - for satisfiable, nothing if not. Explanation:

Ｗ⁻⪪⁻⁻θ(¦)¦>υ⊞υ⌊ι

Extract all of the unique variable names from the input.

⊙…⁰Ｘ²ＬυＵＶ⪫⟦(lambda ⪫λ=0,¦=0:θ)(⪫⮌↨ι²,¦)⟧ω

Compute all possible variable substitutions and evaluate the string as python code with those assignments until one evaluates as True, at which point output a -.

Answer 3

Python3, 397 bytes:

l=len
b=[{'a':0,'b':0,1:0},{'a':0,'b':1,1:0},{'a':1,'b':0,1:1},{'a':1,'b':1,1:0}]
def g(r):
 if len(r)!=len(b[0])-1:return 0
 if all(str==type(i)for i in r):return all(i in b[0]for i in r)
 return any(all(x==y for x,y in zip(r,[*i.values()][:-1])if type(x)==type(y))for i in b)
def f(d):
 if l(d)!=l(b[0])-1:return 0
 if all(j:=[i if isinstance(i,str)else f(i)for i in d]):
  return g(j)
 return 0

Try it online!