Risolutore per trovare i punti fissi di un sistema booleano
Introduzione: il problema
Il mio problema riguarda la risoluzione di un sistema di equazioni che trova il punto fisso di un sistema booleano studiato ($F(X)=X$).
Un semplice esempio
Permettere$\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$essere alcune variabili booleane di interesse. Permettere$F=\{f_1,f_2,f_3\}$essere le funzioni di aggiornamento per queste variabili (es$x_i(t+1) = f_i(x(t))$), definite come le seguenti funzioni di condizione (si basano sugli input di ciascuna variabile - nodo nella concettualizzazione del grafico corrispondente):
$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}$
Queste funzioni sono ispirate da questa domanda .
L'obiettivo è trovare set di risposte $\bar{x}$(potrebbe essere zero, uno o molti di per sé) per cui$F(\bar{x})=\bar{x}$.
L'esempio sopra è ovviamente un caso molto semplice. Alla fine vorrei risolvere tale sistema di equazioni con centinaia di variabili. Si noti che le funzioni di condizione saranno sempre combinazioni lineari degli input di ciascuna variabile e le variabili sempre boolean .
La domanda
Ho bisogno di un risolutore efficiente per questo tipo di problema (che è noto per essere NP-hard tra l' altro!). Ad esempio, questo problema può essere formulato come programmazione a vincoli e risolto utilizzando le tecniche di Answer Set Programming (ASP)?
Risposte
Quindi risulta che ASP può essere utilizzato per risolvere questo problema! Qui fornisco una possibile codifica del problema in un file denominato 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.
Utilizzando clingo(version 5.4.0) dalla riga di comando: clingo fp.lpotteniamo UNSATISFIABLE per questa particolare istanza.
Commentando il fatto %f(2,1,1).ed eseguendo nuovamente il clingorisolutore otteniamo:
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
Le variabili restituite sia nei predicati init/1che in next/1vengono convertite in variabili booleane attive (1) e quelle mancanti in valori inattivi (0). Il risultato restituito è quindi il vettore booleano$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
I crediti per questa risposta vanno a Roland Kaminski. Vari altri membri della comunità ASP potassco hanno fornito utili commenti e soluzioni. Per ulteriori informazioni su ASP, controllare:https://potassco.org/