# Complexity of satisfiability for relational logic on the booleans

I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are relations $$R(x_1,...,x_n)$$ over boolean variables?

Nothing much changes. Every relation $$R(x_1,\dots,x_n)$$ is equivalent to $$\exists t_1,\dots,t_m . \varphi(x_1,\dots,x_n,t_1,\dots,t_m)$$ for some fresh variables $$t_1,\dots,t_m$$ (see the Tseitin transform). Consequently:

Satisfiability remains NP-complete. In particular, satisfiability of $$R(x_1,\dots,x_n)$$ is equivalent to satisfiability of $$\varphi(x_1,\dots,x_n,t_1,\dots,t_m)$$.

Checking formulas with first-order quantifiers remains PSPACE-complete. In particular, the formula $$\forall \cdots \exists . R(x_1,\dots,x_n)$$ is equivalent to $$\forall \cdots \exists . \exists t . \varphi(x_1,\dots,x_n,t_1,\dots,t_m)$$, so the problem is in PSPACE, and it is obviously PSPACE-complete as every formula is itself a relation.

Tautology becomes harder. Tautology of a CNF formula $$\varphi$$ is $$\forall x . \psi(x)$$, which is NP-complete. Tautology of a binary relation $$R$$ is $$\forall x . R(x)$$, which is equivalent to $$\forall x . \exists t . \varphi(x,t)$$, which is believed to be harder than $$\forall x . \psi(x)$$ (NP-complete) or $$\exists x . \psi(x)$$ (co-NP-complete) [unless the polynomial hierarchy collapses].

In NP I could guess the disjunctive normal form of the formulas, that would look like

$$\bigwedge_i R_i(x_1^i, \ldots, x_{n(i)}^i) \land \bigwedge_j \lnot R_j(x_1^j, \ldots, x_{m(j)}^j)$$

The question is then how to decide satisfiability of this term.

One could then take the relation to be the tuple of variables with which they appear in the formula and reduce the problem to finding a satisfying solution of terms of the form $$\lnot (x_1 = x_3 \land x_2 = x_4)$$ where $$R(x_1,x_2)$$ and $$\lnot R(x_3, x_4)$$ occur in the formula above. There are $$O(n^2)$$ such terms thus the problem remains in NP.