Polysat - gromas/polysat GitHub Wiki

При разработке алгоритма используется метод неполной индукции для выявления закономерностей среди случаев, когда формула k-SAT не имеет решений. То есть в настоящий момент я не имею математически точного подтверждения что алгоритм решает проблему P=NP и соответственно не могу гарантировать, что на всех задачах указанный алгоритм не выдаст ложноположительный ответ. Тем не менее, существует гарантия, что алгоритм не выдает ложноотрицательных ответов, каждое ограничение пространства возможных решений проанализировано и для него существует аргументированное математическое обоснование.

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

• Если в каком-то сочетании не существует вектора, совместимого с выбранным, это означает что назначение переменных выбранного вектора невозможно распространить на все переменные решения. В результате чего такой вектор не может являться частью полного назначения и должен быть удалён.