Лекция: Задача выполнимости SAT
В числе важнейших примеров задач удовлетворения ограничений является задача выполнимости SAT. Задача SAT (satisfiability) (задача проверки выполнимости формулы логики высказываний) имеет важное прикладное значение, причем приложения находятся в области автоматического вывода, тестирования электронных схем, баз данных, проектирования компьютеров, анализа изображений, САПР и робототехники.
Именно с задачи SAT Кук (Cook) в 1971 г. начал исследование задач на NP-полноту [28]. Задача SAT состоит в определении, истинна ли данная формула логики высказываний при каком-нибудь значении литералов. Под решением задачи SAT понимается интерпретация, т.е. такое присваивание истинностных значений (1 или 0) литералам в формуле, при которых эта формула станет истинной.
Булева задача выполнимости SAT ‑ это формула, состоящая из трех компонентов:
· множества переменных:
· множества литералов (литерал ‑ это переменная ( ) или отрицание переменной ( ).
· множества различных дизъюнктов:, каждый из которых состоит из литералов, соединенных конъюнкцией ( ).
Цель задачи выполнимости SAT[3] состоит в определении, существует ли присвоение логических значений переменным, которое делает КНФ истинной.
Задача выполнимости SAT ниже, в главе 10, рассматривается как частный случай задачи удовлетворения ограничений.
Здесь используем эквивалентную формулировку задачи SAT в виде задачи ДО без ограничений [35]:
где
Здесь бинарные значения и соответствуют булевым значениям истина и ложь.