MAXIMUM RENAMABLE HORN SUBFORMULA

• 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 $C'\subseteq C$ such that there exists a subset $S \subseteq U$ of the variables such that switching the literals in $S \cup \bar{S}$ makes C' a Horn Boolean formula, where $\bar{S} = \{\bar{u} \mid u \in S\}$.

• MEASURE: The cardinality of the subformula, i.e., $\vert C'\vert$.

  
  

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