# How hard is Heyting satisfiability, i.e. the constructive version of SAT? In particular, is 2-HSAT NL-complete or is it harder?

First of all, is it clear what I mean by $k$-HSAT?

I'm assuming that for $k>2$, $k$-HSAT is NP-complete, but the details of the reductions between $k$-HSAT and $k$-SAT aren't obvious to me.

I'm more curious about whether $2$-HSAT is as easy as $2$-SAT, since as far as I know the latter is easy because, in a Boolean algebra, $a\vee b$ is the same as $\neg a\implies b$, so that a conjunction of clauses of the form $a\vee b$ is just a bunch of implications, and the algorithms I've seen for efficiently solving $2$-SAT use the implication graph that this defines.

• From Wikipedia: The problem of whether a given equation holds in every Heyting algebra was shown to be decidable by S. Kripke in 1965.[1] The precise computational complexity of the problem was established by R. Statman in 1979, who showed it was PSPACE-complete[7] and hence at least as hard as deciding equations of Boolean algebra (shown NP-complete in 1971 by S. Cook)[8] and conjectured to be considerably harder. en.wikipedia.org/wiki/Heyting_algebra Aug 11, 2013 at 19:57
• As I understand it, the question referred to in Wikipedia is still equivalent to satisfiability, but correct me if I'm wrong. Aug 11, 2013 at 19:59
• Sounds like it to me, but it doesn't address the issue of 2-HSAT vs. 2-SAT. Aug 11, 2013 at 20:31
• Agreed. But I don't know enough to answer. Hopefully somebody else will still answer this good question. Aug 12, 2013 at 19:28

First of all, we need to be clear about how we are defining HSAT. Over classical logic we could consider the following two definitions:

1. A formula $\phi(x_1,\ldots,x_n)$ with proposition variables amongst $x_1,\ldots,x_n$ is satisfiable if there are $b_i \in \{\top, \bot\}$ such that $\phi(b_1,\ldots,b_n)$ is true. I'll refer to the corresponding decision problem as SAT.

2. A formula $\phi(x_1,\ldots,x_n)$ with proposition variables amongst $x_1,\ldots,x_n$ is falsifiable (I'm not sure what the standard name for this is) if there are $b_i \in \{\top, \bot\}$ such that $\phi(b_1,\ldots,b_n)$ is not true. I'll refer to the corresponding decision problem as FALSE.

Over classical logic, this isn't such a useful distinction to make, because $\phi$ is satisfiable if and only if $\neg \phi$ is falsifiable (and vice versa). In particular, solving FALSE is equivalent to solving SAT.

By analogy with satisfiability, we could give the following definitions for a propositional formula $\phi(x_1,\ldots,x_n)$:

1. there is a non-trivial Heyting algebra $\mathcal{H}$ and $h_1,\ldots,h_n \in \mathcal{H}$ such that $\phi(h_1,\ldots,h_n) = \top$
2. there is a Kripke model, $\langle W, \leq, \Vdash \rangle$ with root node $0 \in W$, such that $0 \Vdash \phi$
3. $\neg \phi$ is not provable in intuitionistic logic

By applying some soundness and completeness theorems, the three definitions above are equivalent. If they hold for $\phi(x_1,\ldots,x_n)$, say that $\phi$ is H-satisfiable. I'll refer to the corresponding decision problem as HSAT.

By analogy with falsifiability, we could give the following definitions for a propositional formula $\phi(x_1,\ldots,x_n)$:

1. there is a Heyting algebra $\mathcal{H}$ and $h_1,\ldots,h_n \in \mathcal{H}$ such that $\phi(h_1,\ldots,h_n) \neq \top$
2. there is a Kripke model, $\langle W, \leq, \Vdash \rangle$ with root node $0 \in W$, such that $0 \nVdash \phi$
3. $\phi$ is not provable in intuitionistic logic

By applying some soundness and completeness theorems, the three definitions above are equivalent. If they hold for $\phi(x_1,\ldots,x_n)$, say that $\phi$ is H-falsifiable. I'll refer to the corresponding decision problem as HFALSE.

### H-Satisfiability

Note that the correspondence we had before in classical logic no longer holds. In fact, for satisfiability we can say the following. By applying Glivenko's theorem, we can show that $\phi$ is H-satisfiable if and only if it is satisfiable. In particular HSAT is in fact exactly the same problem as SAT and $k$-HSAT is the same as $k$-SAT.

### H-Falsifiability

As Yoav Kallus pointed out in the comment, this is covered in the paper R. Statman, Intuitionistic propositional logic is polynomial-space complete Theoretical Comput. Sci., 9:67{72, 1979. What I called HFALSE is PSPACE-complete.

This only leaves the case of $k$-HFALSE, which unfortunately turns out to not be that interesting. $k$-SAT is the decision problem for formulas in conjunctive normal form whose clauses have at most $k$ variables. Note that if $\phi$ is such a formula, then we can easily put $\neg \phi$ into disjunctive normal form where each conjunctive clause has at most $k$ variables, and vice versa. Hence it makes sense to define $k$-FALSE and $k$-HFALSE as the decision problems for formulas in disjunctive normal form with at most $k$ variables in each clause. In particular, this makes $k$-FALSE equivalent to $k$-SAT.

However, it turns out that for any $\phi$ in disjunctive normal form, $\phi$ is H-falsifiable (by the way, this is also true for conjunctive normal form). You can show this by constructing a Kripke model with two nodes. At the root node set every proposition variable to false and at the other node set every proposition variable to true. For any variable, $x$, neither $x$ nor $\neg x$ holds at the root node, so neither does any formula built from them with only conjunction and disjunction.

So, $k$-HFALSE is trivial.

• The Heyting algebra in the definition of satisfiability had better be nontrivial. Aug 13, 2013 at 11:36
• @EmilJeřábek Yes, I'll correct it.
– aws
Aug 13, 2013 at 11:39