Solver for finding fixpoints of a boolean system

Question

Intro: The Problem

My problem relates to solving a system of equations that find the fixpoint of a studied boolean system ($F(X)=X$).

A Simple Example

Let $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$ be some boolean variables of interest. Let $F=\{f_1,f_2,f_3\}$ be the update functions for these variables (i.e. $x_i(t+1) = f_i(x(t))$), defined as the follow condition functions (they are based on the inputs of each variable - node in the corresponding graph conceptualization):

$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}$

These functions are inspired by this question.

The goal is to to find answer sets $\bar{x}$ (could be zero, one or many per se) for which $F(\bar{x})=\bar{x}$.

The above example is of course a very simple case. In the end I would like to solve such system of equations with hundreds of variables. Note that the condition functions will always be linear combinations of each variable's inputs and the variables always boolean.

The Question

I need an efficient solver for this kind of problem (which is known to be NP-hard btw!). E.g. can this problem formulated as constraint programming and solved using Answer Set Programming (ASP) techniques?

Answer 1

So it turns out that ASP can be used to solve this problem! Here I provide a possible encoding of the problem in a file named 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.

Using clingo (version 5.4.0) from the command line: clingo fp.lp we get UNSATISFIABLE for this particular instance.

Commenting the fact %f(2,1,1). and running again the clingo solver we get:

Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE

Variables that are returned both in the init/1 and next/1 predicates are translated to active boolean variables (1) and those that are missing to inactive values (0). The returned result is thus the boolean vector $\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.

Credits for this answer go to Roland Kaminski. Various other members of the ASP potassco community provided helpful comments and solutions. For more info on ASP, check: https://potassco.org/