3-cnf-sat with a twist question

Question

If you change the 3-cnf-sat problem as follows:
For each c_i, c_i = -x_i1 OR -x_i2 OR x_i3 meaning exactly one of the variables appears without a negation.
You are also given values (0 or 1) to some (or all) of the x's.
You should be able to solve the problem (finding values of the x's that satisfy the problem or prove that it is unsatisfiable) in polynomial time.

1. What is a polynomial running time algorithm that solves this problem?
2. Prove that it runs in polynomial time.

hint: show that c_i = -x_i1 OR -x_i2 OR x_i3 is equal to c = (x_i1 AND -x_i2) -> x_i3

Answer 1

The formulas you describe are a subset of Horn formulas. The satisfiability problem is thus no harder than Horn satisfiability and admits the same linear-time solution.