Mixed Q horn SAT

Question

I am familiar with Horn formula: Formula whose clauses have atmost one positive literal. I am also familiar with Mixed Horn formula: Formula whose clauses are either 2 CNF or Horn.

Question 1: But, what is meant by "mixed Quantified horn formula"?

We also know that, Q3SAT problem: whether a Q3CNF formula is satisfiable.

Question 2:Is there a way to reduce Q3SAT to Mixed Quantified horn SAT problem?

Thank you

Answer 1

A mixed quantified Horn formula is a mixed Horn formula with quantifiers applied to the variables. The Horn CNF formula

$(\lnot x_1\lor x_2) \land (x_1 \lor \lnot x_2 \lor \lnot x_3)$

is the same as the quantified formula

$\exists x_1\exists x_2\exists x_3$ $((\lnot x_1\lor x_2) \land (x_1 \lor \lnot x_2 \lor \lnot x_3))$

because by default existential quantification is assumed for variables in Boolean satisfiability problems. But if quantification is specifically mentioned it usually means that universal quantifiers will also be used. E.g.

$\exists x_1\forall x_2\exists x_3$ $((\lnot x_1\lor x_2) \land (x_1 \lor \lnot x_2 \lor \lnot x_3))$

Satisfying this formula requires that an assignment for $x_1$ exist such that for all assignments to $x_2$ there exists an assignment to $x_3$ that causes the formula to evaluate true. The Wikipedia article on quantified Boolean formulas covers this in greater detail.

As to the second question, whether a quantified 3SAT problem can be reduced to a quantified mixed Horn problem, the answer is yes. Both 3SAT and mixed Horn SAT are NP-complete or $\Sigma_1^P$-complete languages. All NP-complete problems are reducible to each other, as are all $\Sigma_n^P$-complete problems amongst themselves for a given $n$ and all $\Pi_n^P$-complete problems. This covers Q3SAT and quantified mixed Horn SAT.