ブールシステムのフィックスポイントを見つけるためのソルバー
イントロ：問題
私の問題は、研究されたブールシステムの不動点を見つける連立方程式を解くことに関連しています（$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}$ （それ自体がゼロ、1つ、または多数である可能性があります） $F(\bar{x})=\bar{x}$。
上記の例はもちろん非常に単純なケースです。最後に、このような連立方程式を数百の変数で解きたいと思います。条件関数は常に各変数の入力の線形結合であり、変数は常にブール値であることに注意してください。
質問
この種の問題（NP困難であることが知られています！）の効率的なソルバーが必要です。たとえば、この問題は制約プログラミングとして定式化され、Answer Set Programming（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\}$。
この回答のクレジットは、ローランドカミンスキーに送られます。ASPpotasscoコミュニティの他のさまざまなメンバーが有益なコメントと解決策を提供しました。ASPの詳細については、以下を確認してください。https://potassco.org/