SAT с двумя пунктами является полиномиальным

Если я правильно понимаю, это кажется линейным временем в общей длине пунктов.

Унарные предложения немедленно вызывают частичное присваивание переменной. Если какое-либо из двух предложений невыполнимо (пусто) при , или некоторые единичные предложения конфликтуют, экземпляр является невыполнимым. В противном случае экземпляр невыполним только в том случае, если два предложения единичны и дополняют друг друга при , то есть x̅ и x.

В вашей проблеме есть complexity in O(n), где n is the total size of clauses.

У вас есть K унарных предложений, эти K унарных предложений можно рассматривать как подназначение переменных. Если вы не уважаете эти унарные предложения, вы наверняка не найдете решения (если оно существует).

Давайте возьмем пример, чтобы увидеть вашу проблему, цель состоит в том, чтобы найти значения для variables.

 variables = _ _ _ _ _ _ _ _
 problem   = 
              x1                 AND
              x4                 AND
              x7                 AND
             -x8                 AND
             -x5                 AND
              x2                 AND
              x3 OR  -x4 OR x5   AND
              x6 OR  -x1 OR x8

 with K = 5.

Поскольку унарные предложения будут передавать свои значения в variables, эта проблема в основном такая же, как:

 variables = x1 x2 _ x4 -x5 _ x7 -x8
 problem   = 
              x3 OR  -x4 OR  x5  AND
              x6 OR  -x1 OR  x8
 with K = 0.

(Чтобы получить это, мы сделали операцию линейного времени).

И поскольку мы уже знаем значения x4, x5, x1 и x8, эта задача такая же, как:

 variables = x1 x2 _ x4 -x5 _ x7 -x8
 problem   = 
              x3 AND
              x6
 with K = 0.

(Чтобы получить это, мы снова проделали операцию с линейным временем).

А вызвав такую ​​же функцию, как и в первой операции, мы получим:

 variables = x1 x2 x3 x4 -x5 x6 x7 -x8
 problem   = 
              true.
 with K = 0.

(Для получения этого вывода мы снова проделали операцию с линейным временем).

Которые дают вам окончательное решение: variables = x1 x2 x3 x4 -x5 x6 x7 -x8 Как видите, найти решение можно только с помощью операций с линейным временем.