Solucionador para encontrar puntos fijos de un sistema booleano
Introducción: El problema
Mi problema se relaciona con la resolución de un sistema de ecuaciones que encuentra el punto fijo de un sistema booleano estudiado ($F(X)=X$).
Un ejemplo simple
Dejar $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$ser algunas variables booleanas de interés. Dejar$F=\{f_1,f_2,f_3\}$ser las funciones de actualización para estas variables (es decir$x_i(t+1) = f_i(x(t))$), definidas como las siguientes funciones de condición (se basan en las entradas de cada variable - nodo en la conceptualización gráfica correspondiente):
$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}$
Estas funciones están inspiradas en esta pregunta .
El objetivo es encontrar conjuntos de respuestas $\bar{x}$ (podría ser cero, uno o muchos per se) para el cual $F(\bar{x})=\bar{x}$.
El ejemplo anterior es, por supuesto, un caso muy simple. Al final, me gustaría resolver ese sistema de ecuaciones con cientos de variables. Tenga en cuenta que las funciones de condición siempre serán combinaciones lineales de las entradas de cada variable y las variables siempre serán booleanas .
La pregunta
Necesito un solucionador eficiente para este tipo de problema (¡que se sabe que es NP-hard por cierto!). Por ejemplo, ¿puede este problema formularse como programación de restricciones y resolverse utilizando técnicas de programación de conjuntos de respuestas (ASP)?
Respuestas
¡Entonces resulta que ASP se puede usar para resolver este problema! Aquí proporciono una posible codificación del problema en un archivo llamado 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.
Usando clingo(versión 5.4.0) desde la línea de comando: clingo fp.lpobtenemos INSATISFIABLE para esta instancia en particular.
Comentando el hecho %f(2,1,1).y ejecutando nuevamente el clingosolucionador obtenemos:
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
Las variables que se devuelven en los predicados init/1y next/1se traducen en variables booleanas activas (1) y las que faltan en valores inactivos (0). El resultado devuelto es, por tanto, el vector booleano$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
Los créditos por esta respuesta son para Roland Kaminski. Varios otros miembros de la comunidad ASP potassco proporcionaron comentarios y soluciones útiles. Para obtener más información sobre ASP, consulte:https://potassco.org/