Истинные квантифицированные булевы формулы в недетерминированных задачах с полиномиальным временем
Первый подход к пониманию того, как их соединить
Представьте, что у вас есть механизм, который даже вручную позволяет связать любое количественное логическое выражение с простым выражением без квантификаторов.
Представьте, что, кроме того, вы включаете механизмы, которые позволяют разрешать любое логическое выражение за полиномиальное время ...
Но пока никто тебе не верит. У вас есть алгоритмы, дотошные объяснения… но официально вы еще не получили отрицания или одобрения.
В этом посте я покажу ядро связи между TQBF, чтобы участвовать в классе NP.
Что означает TQBF
Истинные квантифицированные логические формулы означает, что у вас есть логическое выражение и вы хотите знать, могут ли некоторые из его переменных быть выражены как логическая функция, чтобы превратить все выражение в тавтологию. Это как сказать: если логическое выражение с его переменными и параметрами является теоремой. Например, ⱯP ⱯQ: P & (P → Q) → Q - это QBF и ⱯP ⱯQ: P & (P → Q) → Q = 1 - это TQBF.
TQBF - это своего рода проблема, истинно ли выражение, если все переменные имеют вид Ɐ, это означает, что мы работаем с возможной тавтологией. В нашем примере: (P → Q) → Q = 1 - тавтология означает:
- ¬ (ⱻP, ⱻQ: ¬ (P & (P → Q) → Q) = 1)
Это похоже на решение TBF: ¬ (P & (P → Q) → Q) и ответ на проблему, противоположную TQBF.
Итак, возникает вопрос: что мы можем сделать с выражениями, имеющими экзистенциальный характер, например: ⱯP ⱻQ: (P → Q) → ¬P.
Вначале следует сказать, что ставить экзистенциальное (ⱻ) перед универсальным (Ɐ) - это не одно и то же.
- В ⱻQⱯP: (P → Q) → ¬P, Q не может зависеть от P
- В ⱯP ⱻQ: (P → Q) → ¬P, Q - это логическое выражение, зависящее от P или нет
В первом случае Q может получить только два возможных значения (True или False), если вы попытаетесь найти тавтологию в Q = Ложь:
- (Истина → Ложь) → Ложь = Истина → Ложь = Ложь
- (Ложь → Ложь) → Истина = Истина → Истина = Истина
Итак, если Q = False, это не тавтология.
Если Q = Верно:
- (Истина → Истина) → Ложь = Истина → Ложь = Ложь
- (Ложь → Истина) → Истина = Истина → Истина = Истина
Это означает, что выражение: ⱻQⱯP: (P → Q) → ¬P не является логической теоремой.
Но если мы проверим Q = ¬P в ⱯP ⱻQ: (P → Q) → ¬P,
- (Истина → Ложь) → Ложь = Ложь → Ложь = Истина
- (Ложь → Истина) → Истина = Истина → Истина = Истина
Итак, ⱯP ⱻQ: (P → Q) → ¬P - это булева теорема, и мы можем достичь только одной тавтологии в Q = ¬P, , и вы можете прочитать это так: если выражение указывает на свое противоречие, оно указывает на противоположное выражению.
Представляете, сколько приложений мы смогли бы сделать, если бы смогли найти выражение, порождающее тавтологию.
Что такое предложения Хорна?
Чтобы было проще, я рекомендую работать с клаузулами Хорна. Представьте, что каждое логическое выражение преобразуется в продукт предложений Хорна:
Каждое предложение формы (A1 + A2 +… + An + ¬B1 + ¬B2 +… + ¬Bn) преобразуется в форму: (B1 & B2 &… & Bn → A1 + A2 +… + An), поэтому что мы можем избежать негативных форм.
Если мы добавим пункты формы:
- (Верно → A1 +… + An) и
- (B1 &… & Bn → Ложь)
Затем результат этих предложений будет представлять каждое логическое выражение.
Итак, что делает тавтологию оговоркой Хорна?
Реализация ParamClause
Мы можем изучить предложения Horn, работая с Pandas. Учитывая, насколько это может быть полезно для огромных баз данных.
Чтобы понять, как это работает, мы можем начать с предложения Quantified Horn:
- Ɐx, Ɐy, Ɐz, ⱻA, ⱻB: A & x → B + y + z
Выражение выше имеет два параметра A, B и три переменные x, y, z . Если мы рассмотрим возможные выражения, которые формула может принимать для каждого параметра, мы могли бы сказать, что если бы A, например, было False, все предложение уже было бы тавтологией .
Более конкретно: (A = False) + (A = ¬ x) + (A = y) + (A = z ), и вы можете выразить эти четыре возможности в строке с логикой из трех значений как A: ”2211 '. Это означает, что 1 - Истина, 2 - Ложь, 3 - Не определено. Если он связан с переменной x: 1 - это x, 2 - это ¬x, а 3 - Несвязанный.
Итак, представьте, что вы можете ввести формулу A & x → B + y + z следующим образом:
>>> ParamClause("22111122", "A", "B")
Clause of 2 params.
A B
0 2 1
1 2 1
2 1 2
3 1 2
В этой версии переменные x, y, z не упоминаются, но 1, 2, 3; и это код:
from pandas import DataFrame
class ParamClause:
'Clauses of at least one parameter recognized'
def __init__(self, body, *params):
self.body = DataFrame({params[j] : X \
for j, X in enumerate(
ParamClause.sequence(body, len(params)))})
@staticmethod
def sequence(body, nParams):
body = [3 if not x in '12' else int(x) for x in body]
n = len(body)//nParams
return [body[i * n: (i + 1) * n] for i in range(nParams)]
def __repr__(self):
return 'Clause of '\
+repr(self.body.shape[1]) + ' params.\n' \
+ repr(self.body)
С этого момента вы можете легко представить, как преобразовать проблему выполнимости логического выражения. Потому что, если у вас было два предложения Horn, объекты ParamClause должны иметь общие параметры и переменные, и в этой точке вы должны использовать третье значение (3), избегайте какой-либо связи переменной с предложением или параметром.
С помощью этого метода:
def required(self):
return [(I, J) for I in self.body.columns \
for J in self.body.index if self.body[I][J]<3]
Вы можете получить доступ к каждой логической переменной, чтобы удовлетворить следующие запросы:
>>> ParamClause("22111122", "A", "B").required()
[('A', 0), ('A', 1), ('A', 2), ('A', 3), ('B', 0), ('B', 1), ('B', 2), ('B', 3)]
Пара (столбец, строка) кодирует логическую переменную, которая иногда заключена в разных предложениях, чтобы генерировать формулу.
Старая версия
В quantifiers31.py вы можете получить полный код, а не в пандах, который генерирует окончательную логическую формулу.
В этой версии вы могли использовать объект, содержащий список объектов QTuple (объекты ParamClause), и после выполнения формулы он генерирует QTuple Решение получить любой из всех случаев тавтологии.
В нашем классе ParamClause нам нужно будет реализовать методы:
def notNulledParams(self):
return [X for X in self.body.columns \
if (self.body[X] == 3).sum() < self.body.shape[0]]
def compatiblesInParam(self, other, param):
return (self.body[param] \
& other.body[param] == 0).sum() == 0
Что очень просто с пандами. На данный момент у меня нет полной версии, но если этот пост сочтут интересным, я могу закончить этот урок с помощью панд.
Конечно, вы можете поделиться или попробовать все в этом общедоступном коде.
