3-cnf-sat с неожиданным вопросом

Если вы измените задачу 3-cnf-sat следующим образом:
Для каждого c_i, c_i = -x_i1 ИЛИ -x_i2 ИЛИ x_i3 означает, что ровно одна из переменных появляется без отрицания.
Вам также присваиваются значения (0 или 1) для некоторых (или всех ) из x.
Вы должны быть в состоянии решить задачу (найти значения x, которые удовлетворяют задаче или доказывают ее невыполнимость) за полиномиальное время.

1. Какой алгоритм с полиномиальным временем выполнения решает эту задачу?
2. Докажите, что оно выполняется за полиномиальное время.

Подсказка: покажите, что c_i = -x_i1 ИЛИ -x_i2 ИЛИ x_i3 равно к c = (x_i1 AND -x_i2) -> x_i3