On the Approximability of Splitting-SAT in 2-CNF Horn Formulas

Splitting a variable in a Boolean formula means to replace an arbitrary set of its occurrences by a new variable. In the minimum splitting SAT problem, we ask for a minimum-size set of variables to be split in order to make the formula satisfiable. This problem is known to be APX-hard, even for 2-CNF formulas. We consider the case of 2-CNF Horn formulas, i.e., 2-CNF formulas without positive 2-clauses, and prove that this problem is APX-hard as well. We also analyze subcases of 2-CNF Horn formulas, where additional clause types are forbidden. While excluding negative 2-clauses admits a polynomial-time algorithm based on network flows, the splitting problem stays APX-hard for formulas consisting of positive 1-clauses and negative 2-clauses only.

Instead of splitting as many variables as possible to make a formula satisfiable, one can also look at the dual problem of finding the maximum number of variables that can be assigned without violating a clause. We also study the approximability of this maximum assignment problem on 2-CNF Horn formulas. While the polynomially solvable subproblems are the same as for the splitting problem, the maximum assignment problem in general Horn formulas is as hard to approximate as the maximum independent set problem.