3-cnf-sat with twist issue

Question

If you change the problem with 3-cnf-sat as follows:
For each c _i , c _i = -x _i1 OR -x _i2 OR x _i3 means that only one of the variables appears without negation.
You are also assigned values ​​(0 or 1) to some (or all) x.
You have to solve the problem (find the values ​​of x that satisfy the problem or prove that it is unsatisfactory) in polynomial time.

• What is a polynomial runtime algorithm that solves this problem?
• 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 that you describe are a subset of the Horn formulas. Thus, the feasibility problem is no more complicated than the Horn feasibility and admits the same linear time solution.