Solveur pour trouver les points fixes d'un système booléen
Intro: Le problème
Mon problème concerne la résolution d'un système d'équations qui trouve le point fixe d'un système booléen étudié ($F(X)=X$).
Un exemple simple
Laisser $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$être des variables booléennes d'intérêt. Laisser$F=\{f_1,f_2,f_3\}$être les fonctions de mise à jour de ces variables (ie$x_i(t+1) = f_i(x(t))$), définies comme les fonctions de condition suivantes (elles sont basées sur les entrées de chaque variable - nœud dans la conceptualisation graphique correspondante):
$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}$
Ces fonctions sont inspirées de cette question .
Le but est de trouver des ensembles de réponses $\bar{x}$ (peut être zéro, un ou plusieurs en soi) pour lesquels $F(\bar{x})=\bar{x}$.
L'exemple ci-dessus est bien sûr un cas très simple. En fin de compte, je voudrais résoudre un tel système d'équations avec des centaines de variables. Notez que les fonctions de condition seront toujours des combinaisons linéaires des entrées de chaque variable et les variables toujours booléennes .
La question
J'ai besoin d'un solveur efficace pour ce genre de problème (qui est connu pour être NP-hard btw!). Par exemple, ce problème peut-il être formulé sous forme de programmation par contraintes et résolu à l'aide des techniques de programmation par jeu de réponses (ASP)?
Réponses
Il s'avère donc que ASP peut être utilisé pour résoudre ce problème! Ici, je fournis un encodage possible du problème dans un fichier nommé 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.
En utilisant clingo(version 5.4.0) à partir de la ligne de commande: clingo fp.lpnous obtenons UNSATISFIABLE pour cette instance particulière.
En commentant le fait %f(2,1,1).et en exécutant à nouveau le clingosolveur nous obtenons:
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
Les variables renvoyées à la fois dans les prédicats init/1et next/1sont converties en variables booléennes actives (1) et celles qui manquent en valeurs inactives (0). Le résultat renvoyé est donc le vecteur booléen$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
Les crédits pour cette réponse vont à Roland Kaminski. Divers autres membres de la communauté ASP potassco ont fourni des commentaires et des solutions utiles. Pour plus d'informations sur ASP, consultez:https://potassco.org/