This is Post's lattice:

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.


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


This is a decision problem so you should have two distinct output values for SAT and UNSAT. Use a reasonable input format. For example:


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


3 Answers 3


Wolfram Language (Mathematica), 30 bytes


Try it online!

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


Charcoal, 57 bytes

W⁻⪪⁻⁻θ(¦)¦>υ⊞υ⌊ι⊙…⁰X²LυUV⪫⟦(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.

⊙…⁰X²LυUV⪫⟦(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 -.


Python3, 397 bytes:

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!


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.