Выполнимость

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

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

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

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

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

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

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

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

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

А ⊧ φ [а]

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

А ⊧ φ

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

А ⊧ Т

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

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

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

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

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

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

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

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

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

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

• 2-выполнимость
• Проблема выполнимости булевых уравнений
• Выполнимость схемы
• 21 NP-полная задача Карпа
• Действительность
• Удовлетворение ограничений

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

• Daniel Kroening ; Ofer Strichman (2008). Процедуры принятия решений: алгоритмическая точка зрения . Springer Science & Business Media. ISBN 978-3-540-74104-6.
• A. Biere; M. Heule; H. van Maaren; T. Walsh, ред. (2009). Справочник по выполнимости . IOS Press. ISBN 978-1-60750-376-7.