Решатель для поиска фиксированных точек булевой системы
Вступление: Проблема
Моя проблема связана с решением системы уравнений, которая находит фиксированную точку исследуемой булевой системы ($F(X)=X$).
Простой пример
Позволять $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$- интересующие вас логические переменные. Позволять$F=\{f_1,f_2,f_3\}$быть функциями обновления для этих переменных (т.е.$x_i(t+1) = f_i(x(t))$), определяемые как следующие функции условий (они основаны на входных данных каждой переменной - узла в соответствующей концептуализации графа):
$f_1 = \begin{cases} 1, -x_2 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_2 = \begin{cases} 1, x_1-x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_3 = \begin{cases} 1, x_1+x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$
Эти функции навеяны этим вопросом .
Цель - найти наборы ответов $\bar{x}$ (может быть ноль, один или несколько), для которых $F(\bar{x})=\bar{x}$.
Приведенный выше пример, конечно, очень простой случай. В конце концов, я хотел бы решить такую систему уравнений с сотнями переменных. Обратите внимание, что функции условий всегда будут линейными комбинациями входных данных каждой переменной, а переменные всегда будут логическими .
Вопрос
Мне нужен эффективный решатель для такого рода проблем (который, кстати, известен как NP-трудный !). Например, можно ли эту проблему сформулировать как программирование с ограничениями и решить с помощью методов программирования набора ответов (ASP)?
Ответы
Получается, что для решения этой проблемы можно использовать ASP! Здесь я предоставляю возможную кодировку проблемы в файле с именем fp.lp:
% variables
var(1..3).
% functions
% f(Function,Coefficient,Variable)
f(1,-1,2).
f(2,1,1).
f(2,-1,3).
f(3,1,1).
f(3,1,3).
% guess assignment to variables
{ init(V) : var(V) }.
% compute functions
next(F) :- var(F), #sum { C,V : f(F,C,V), init(V) } >= 0.
% check if fixed point
:- init(V), not next(V).
:- next(V), not init(V).
#show next/1.
#show init/1.
Используя clingo(версию 5.4.0) из командной строки: clingo fp.lpмы получаем НЕУДОВЛЕТВОРЕННЫЙ для этого конкретного экземпляра.
Комментируя факт %f(2,1,1).и снова запуская clingoрешатель, получаем:
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
Переменные, которые возвращаются как в init/1и next/1предикаты преобразуются в активные логические переменные (1) и те , которые отсутствуют в неактивные значения (0). Таким образом, возвращаемый результат - это логический вектор$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
Кредиты за этот ответ принадлежат Роланду Камински. Различные другие члены сообщества ASP potassco предоставили полезные комментарии и решения. Для получения дополнительной информации об ASP проверьте:https://potassco.org/