First of all, we need to be clear about how we are defining HSAT. Over classical logic we could consider the following two definitions:
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.
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)$:
- 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$
- there is a Kripke model, $\langle W, \leq, \Vdash \rangle$ with root node $0 \in W$, such that $0 \Vdash \phi$
- $\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)$:
- 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$
- there is a Kripke model, $\langle W, \leq, \Vdash \rangle$ with root node $0 \in W$, such that $0 \nVdash \phi$
- $\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.
