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.