- INSTANCE: Set
*U*of variables, collection*C*of conjunctive clauses of at most 3 literals, where a literal is a variable or a negated variable in*U*. - SOLUTION: A renamable Horn subformula
*C'*of*C*, i.e., a subset such that there exists a subset of the variables such that switching the literals in makes*C'*a Horn Boolean formula, where . - MEASURE: The cardinality of the subformula, i.e., .

*Good News:*Approximable within 40/67 [91].