Удовлетворенность

В математической логике формула если является выполнимой, она истинна при некотором присвоении значений ее переменным . Например, формула $x+3=y$ выполнимо, поскольку оно истинно, когда $x=3$ и $y=6$ , а формула $x+1=x$ не выполнимо в целых числах. Двойственной концепцией выполнимости является валидность ; Формула действительна , если каждое присвоение значений ее переменным делает формулу истинной. Например, $x+3=3+x$ справедливо для целых чисел, но $x+3=y$ нет.

Формально выполнимость изучается относительно фиксированной логики, определяющей синтаксис разрешенных символов, таких как логика первого порядка , логика второго порядка или логика высказываний . Однако выполнимость является не синтаксическим свойством, а семантическим свойством, поскольку она связана со значением символов, например, со значением $+$ в такой формуле, как $x+1=x$ . Формально мы определяем интерпретацию (или модель ) как присвоение значений переменным и присвоение значения всем другим нелогическим символам, а формула считается выполнимой, если существует некоторая интерпретация, которая делает ее истинной. ^[1] Хотя это допускает нестандартные интерпретации символов, таких как $+$ , можно ограничить их смысл, предоставив дополнительные аксиомы . Проблема выполнимости по модулю теорий рассматривает выполнимость формулы относительно формальной теории , которая представляет собой (конечный или бесконечный) набор аксиом.

Выполнимость и обоснованность определяются для одной формулы, но могут быть обобщены на произвольную теорию или набор формул: теория выполнима, если хотя бы одна интерпретация делает каждую формулу теории истинной, и действительна, если каждая формула верна в любой интерпретации. . Например, теории арифметики, такие как арифметика Пеано, выполнимы, потому что они верны в натуральных числах. Эта концепция тесно связана с непротиворечивостью теории и фактически эквивалентна непротиворечивости логики первого порядка — результат, известный как теорема Гёделя о полноте . Отрицание выполнимости есть невыполнимость, а отрицание действительности есть недействительность. Эти четыре понятия связаны друг с другом точно так же, как Аристотеля оппозиции квадрат .

Проблема определения того , является ли формула в логике высказываний выполнимой , разрешима и известна как проблема булевой выполнимости , или SAT. В общем случае проблема определения выполнимости предложения логики первого порядка неразрешима. В универсальной алгебре , эквациональной теории и автоматизированном доказательстве теорем методы переписывания терминов , замыкания сравнения и унификации используются для попытки определить выполнимость. Разрешимость той или иной теории или нет зависит от того, является ли она без переменных и от других условий. ^[2]

Сведение валидности к выполнимости

Для классической логики с отрицанием, как правило, можно переформулировать вопрос о применимости формулы к вопросу о выполнимости из-за отношений между понятиями, выраженными в приведенном выше квадрате оппозиции. В частности, φ действителен тогда и только тогда, когда ¬φ невыполнимо, то есть ложно, что ¬φ выполнимо. Другими словами, φ выполнима тогда и только тогда, когда ¬φ недействителен.

Для логик без отрицания, таких как положительное исчисление высказываний , вопросы достоверности и выполнимости могут быть не связаны между собой. В случае позитивного исчисления высказываний проблема выполнимости тривиальна, поскольку каждая формула выполнима, а проблема достоверности является ко-NP полной .

Пропозициональная выполнимость классической логики

В случае классической логики высказываний выполнимость разрешима для формул высказываний. В частности, выполнимость является NP-полной проблемой и одной из наиболее интенсивно изучаемых проблем в теории сложности вычислений .

Выполнимость в логике первого порядка

Для логики первого порядка (FOL) выполнимость неразрешима . Точнее, это ко-RE-полная задача и, следовательно, не полуразрешимая . ^[3] Этот факт связан с неразрешимостью проблемы достоверности ВОЛС. Вопрос о статусе проблемы достоверности был поставлен впервые Дэвидом Гильбертом как так называемая Entscheidungsproblem . Универсальная применимость формулы является полуразрешимой проблемой согласно теореме Гёделя о полноте . Если бы выполнимость также была полуразрешимой проблемой, то и проблема существования контрмоделей была бы такой же (формула имеет контрмодели тогда и только тогда, когда ее отрицание выполнимо). Таким образом, проблема логической достоверности будет разрешима, что противоречит теореме Чёрча-Тьюринга , результату, дающему отрицательный ответ на проблему Entscheidungs.

Выполнимость в теории моделей

В теории моделей атомарная формула является выполнимой, если существует набор элементов структуры , которые делают формулу истинной. ^[4] Если A — структура, φ — формула и a — набор элементов, взятых из структуры, удовлетворяющих φ, то обычно пишут, что

А ⊧ φ [а]

Если φ не имеет свободных переменных, то есть если φ — атомарное предложение и ему удовлетворяет A , то пишут

А ⊧ е

В этом случае можно также сказать, что A является моделью для φ или что φ истинно в A . Если T — это набор атомарных предложений (теория), которым удовлетворяет A , пишут

А ⊧ Т

Конечная выполнимость

Проблема, связанная с выполнимостью, — это проблема конечной выполнимости , которая заключается в определении того, допускает ли формула конечную модель, которая делает ее истинной. Для логики, обладающей свойством конечной модели , проблемы выполнимости и конечной выполнимости совпадают, поскольку формула этой логики имеет модель тогда и только тогда, когда она имеет конечную модель. Этот вопрос важен в математической области теории конечных моделей .

Конечная выполнимость и выполнимость, вообще говоря, не обязательно должны совпадать. Например, рассмотрим логическую формулу первого порядка, полученную как соединение следующих предложений, где $a_{0}$ и $a_{1}$ являются константами :

$R(a_{0},a_{1})$
$\forall xy(R(x,y)\rightarrow \exists zR(y,z))$
$\forall xyz(R(y,x)\wedge R(z,x)\rightarrow y=z))$
$\forall x\neg R(x,a_{0})$

Полученная формула имеет бесконечную модель $R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ , но можно показать, что он не имеет конечной модели (начиная с того, что $R(a_{0},a_{1})$ и следуя по цепочке $R$ атомов , которые должны существовать согласно второй аксиоме, конечность модели потребует существования петли, которая нарушит третью и четвертую аксиомы, независимо от того, зацикливается ли она снова $a_{0}$ или на другом элементе).

Вычислительная сложность определения выполнимости входной формулы в данной логике может отличаться от сложности определения конечной выполнимости; фактически для некоторых логик разрешима только одна из них .

Для классической логики первого порядка конечная выполнимость рекурсивно перечислима (в классе RE ) и неразрешима по теореме Трахтенброта, примененной к отрицанию формулы.

Числовые ограничения

Числовые ограничения ^{[ объяснить ]} часто появляются в области математической оптимизации , где обычно хотят максимизировать (или минимизировать) целевую функцию с учетом некоторых ограничений. Однако, если оставить в стороне целевую функцию, основной вопрос простого решения о том, выполнимы ли ограничения, в некоторых ситуациях может оказаться сложной или неразрешимой. В следующей таблице приведены основные случаи.

Ограничения	над реальными	над целыми числами
Линейный	PTIME (см. линейное программирование )	NP-полный (см. целочисленное программирование )
Полиномиальный	разрешимо, например, посредством цилиндрического алгебраического разложения	неразрешима ( десятая проблема Гильберта )

Источник таблицы: Бокмайр и Вайспфеннинг . ^[5]^: 754

Для линейных ограничений более полную картину дает следующая таблица.

Ограничения превышены:	рациональное объяснение	целые числа	натуральные числа
Линейные уравнения	ПТАЙМ	ПТАЙМ	NP-полный
Линейные неравенства	ПТАЙМ	NP-полный	NP-полный

Источник таблицы: Бокмайр и Вайспфеннинг . ^[5]^: 755

См. также

Примечания

^ Булос, Берджесс и Джеффри 2007 , стр. 120: «Набор предложений [...] выполним , если некоторая интерпретация [делает его истинным]».
^ Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета. стр. 58–92. ISBN 0-521-77920-0 .
^ Байер, Кристель (2012). «Глава 1.3 Неразрешимость ВОЛС» . Конспект лекций — Продвинутая логика . Technische Universität Dresden — Институт технической информатики. стр. 28–32. Архивировано из оригинала (PDF) 14 октября 2020 года . Проверено 21 июля 2012 г.
^ Уилфрид Ходжес (1997). Теория более коротких моделей . Издательство Кембриджского университета. п. 12. ISBN 0-521-58713-1 .
^ Jump up to: ^а ^б Александр Бокмайр; Фолькер Вайспфеннинг (2001). «Решение числовых ограничений». У Джона Алана Робинсона; Андрей Воронков (ред.). Справочник по автоматизированному рассуждению, том I. Elsevier и MIT Press. ISBN 0-444-82949-0 . (Эльзевир) (MIT Press).

Ссылки

Булос, Джордж; Берджесс, Джон; Джеффри, Ричард (2007). Вычислимость и логика (5-е изд.). Издательство Кембриджского университета.

Дальнейшее чтение

Дэниел Кренинг ; Офер Стрихман (2008). Процедуры принятия решений: алгоритмическая точка зрения . Springer Science & Business Media. ISBN 978-3-540-74104-6 .
А. Бьер; М. Хёле; Х. ван Маарен; Т. Уолш, ред. (2009). Справочник по выполнимости . ИОС Пресс. ISBN 978-1-60750-376-7 .

[FOOTNOTEBoolosBurgessJeffrey2007p._120:_"A_set_of_sentences_[...]_is_''satisfiable''_if_some_interpretation_[makes_it_true]."-1] Булос, Берджесс и Джеффри 2007 , стр. 120: «Набор предложений [...] выполним , если некоторая интерпретация [делает его истинным]».

[2] Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета. стр. 58–92. ISBN 0-521-77920-0 .

[3] Байер, Кристель (2012). «Глава 1.3 Неразрешимость ВОЛС» . Конспект лекций — Продвинутая логика . Technische Universität Dresden — Институт технической информатики. стр. 28–32. Архивировано из оригинала (PDF) 14 октября 2020 года . Проверено 21 июля 2012 г.

[4] Уилфрид Ходжес (1997). Теория более коротких моделей . Издательство Кембриджского университета. п. 12. ISBN 0-521-58713-1 .

[BockmayrWeispfenning2001-5] Jump up to: ^а ^б Александр Бокмайр; Фолькер Вайспфеннинг (2001). «Решение числовых ограничений». У Джона Алана Робинсона; Андрей Воронков (ред.). Справочник по автоматизированному рассуждению, том I. Elsevier и MIT Press. ISBN 0-444-82949-0 . (Эльзевир) (MIT Press).

[1]

[2]

[3]

[4]

[5]