# What complexity class is this set of grammars? In between NL and P?

Given a grammar where (every rule has the form $$X \to YZ$$, $$XY \to Z$$ or $$X \to a$$), (($$X \to YZ$$) implies ($$X \to ZY$$)) and (($$XY \to Z$$) implies ($$YX \to Z$$)) where $$X,Y,Z$$ range over nonterminals and $$a$$ ranges over terminals, and given a nonterminal $$S$$ and a terminal $$a$$, determine whether $$S$$ can derive $$a$$.

What complexity class does this correspond to?

It appears to be the problem of finding an "all-in-path" in a "3-digraph" (See: Is there a name for this directed graph and path concept? 3-digraph and all-in-path?).

Related questions:

What complexity class does is this set of grammars? L-complete?

What complexity class does is this set of grammars? NL-complete?

What complexity class is this set of grammars?

What complexity class is this set of grammars? RE?

This appears "almost P-complete".

I think this is existential and P-complete is universal.

This problem corresponds to, "given (1) a SAT problem, (2) a candidate solution, and (3) a variable A, does (A imply (not A))?" This problem shows the existence of a contradiction (for a single variable).

P-complete corresponds to "given (1) a SAT problem, and (2) a candidate solution, does there exist a variable X such that (X implies (not X))?" By showing there exists a solution, you show the non-existence of a contradiction (for all variables).

Sometimes it's easier to find a contradiction than a solution. Consider a Horn-SAT problem containing the clauses A and (not A). You don't need to check the other clauses.

This assumes the original question is equivalent to finding an "all-in-path" in a "3-digraph" (See: Is there a name for this directed graph and path concept? 3-digraph and all-in-path?

Given a 3-SAT instance S, candidate solution Candidate and a target variable, X, does X imply not X?

We will construct a 3-digraph:

For each literal A and its negation nA, in S, create a vertex.

Rewrite each or-clause in S:

(A or B or C)

((A or B) or C)

(not(not((A or B))) or C)

(not(not(A) and not(B))) or C)

(not(A) and not(B)) implies C)

Since there are 6 permutations of A,B,C, there are 6 rewrites. For each rewrite, add 2 directed edges: nA->C and nB->C.

Create a new vertex, Candidate. For each literal A in Candidate, add a directed edge Candidate->A.

Create a new vertex, XContradiction. Add directed edges X->Xcontradiction nX->Xcontradiction.

(After adding edges, ensure this is a trigraph.)

Is there an all-in-path from S to Xcontradiction?

If we show the non-existence of an all-in-path for each literal (and not just X), then we have decided the corresponding P problem (does Candidate satisfy).