Skip to content

Алгоритм решения задач выполнимости булевой формулы 3-SAT

License

Notifications You must be signed in to change notification settings

gromas/3-SAT-solver-algorithm

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

13 Commits
 
 
 
 

Repository files navigation

3-SAT-solver-algorithm

Алгоритм решения задач выполнимости булевой формулы 3-SAT с заранее определенной сложностью

Простой алгоритм, позволяющий решить любую задачу, представленную в виде 3-SAT выражения
Сложность в лучшем случае O(2n)

  1. Создадим пустой массив переменных P.
  2. В выражении выберем переменную xi такую, что бы она входила в максимальное число клозов (дизъюнктов). Запишем эту переменную в массив P. Разделим функцию на две части - в левой части оставим клозы, в которые xi не входит, в правую перенесём все клозы, в которые xi входит. Будем выполнять пункт 2 на левой части функции до тех пор, пока в ней не останется клозов.
  3. Утверждение: перебор переменных массива P всегда обращает исходную функцию в 2SAT выражение, которое решается за линейное время.
  4. Полный перебор переменных массива P гарантированно находит решение 3SAT выражения.
  5. Лучшее время выполнения определяется сложностью функции и может быть минимально равно O(2n), если первая же выбранная переменная xi входит во все клозы выражения.

image

На представленном выше рисунке видно, что при подстановке всех значений в массив P выражение обращается в 2-SAT выражение Перебирая все варианты в массиве P мы получим все возможные 2-SAT выражения Решив их мы найдем, что функция или имеет решение или не имеет, если все варианты перебора возвратили 2-SAT выражения, не имеющие решения.

Удачи, R5FO

Ссылка на обсуждение в telegram: https://t.me/hamrecipe/35?comment=165

About

Алгоритм решения задач выполнимости булевой формулы 3-SAT

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published