Задача выполнимости SAT

В числе важнейших примеров задач удовлетворения ограничений является задача выполнимости SAT. Задача SAT (satisfiability) (задача проверки выполнимости формулы логики высказываний) имеет важное прикладное значение, причем приложения находятся в области автоматического вывода, тестирования электронных схем, баз данных, проектирования компьютеров, анализа изображений, САПР и робототехники.

Именно с задачи SAT Кук (Cook) в 1971 г. начал исследование задач на NP-полноту [28]. Задача SAT состоит в определении, истинна ли данная формула логики высказываний при каком-нибудь значении литералов. Под решением задачи SAT понимается интерпретация, т.е. такое присваивание истинностных значений (1 или 0) литералам в формуле, при которых эта формула станет истинной.

Булева задача выполнимости SAT ‑ это формула, состоящая из трех компонентов:

· множества переменных:

· множества литералов (литерал ‑ это переменная () или отрицание переменной ().

· множества различных дизъюнктов: , каждый из которых состоит из литералов, соединенных конъюнкцией ().

Цель задачи выполнимости SAT[3] состоит в определении, существует ли присвоение логических значений переменным, которое делает КНФ истинной.

Задача выполнимости SAT ниже, в главе 10, рассматривается как частный случай задачи удовлетворения ограничений.

Здесь используем эквивалентную формулировку задачи SAT в виде задачи ДО без ограничений [35]:

где

Здесь бинарные значения и соответствуют булевым значениям истина и ложь.