Алгоритм булевой выполнимости -

У меня есть логическая формула:(х _{1} или х _{2} )и (х _{3} или х _{4} )и..... и (х _{2r -1} или х _{2r}), где x _{i} принадлежит множеству:{p _{1}, p _{2},... p _{99}, ~p _{1}, ~p _{2},... ~p _{99} } и я должен определить, может ли данная формула быть верной для некоторых значений x _{i} .

Я знаю, что это вообще вычислительно сложно. Но есть ли какой-нибудь довольно быстрый способ решить эту конкретную проблему? До сих пор я пробовал откат -, который находится в рекурсии. Я подставляю каждое возможное значение (0 или 1, так что не так много )для каждой возможной переменной, и каждая переменная, которая еще не получила значения, тривиально верна. Прежде чем углубиться в рекурсию, я проверяю формулу (, даже если не каждая переменная имеет значение ), и если оно ложно, я не углубляюсь. Но это слишком медленно. Любые идеи? Буду очень благодарен за помощь.