Horn SAT
(library/algorithm/horn_sat.hpp)
Horn SAT
以下の形式で表される充足可能性問題を解きます。
\[\bigwedge_{i=1}^M \left(\left(x_{a^i_1}\land x_{a^i_2}\land\cdots\land x_{a^i_{c_i}}\right)\to y_{b_i}\right)\tag{1}\]
ここで、$x$ は正リテラルに限ります ($y$ の正負は問いません)。
コンストラクタ
条件節の追加
充足可能性判定
解の例示
-
シグネチャ
const std::vector<bool>& answer()
-
概要
今までに与えた条件節たちをすべて満たすような真偽値の割り当て方が存在するならば、そのような割り当てを一つ返します。
Note: 必ず先に satisfiable
を呼んでください。satisfiable
を呼ばなかった場合、または satisfiable
を呼んで返り値が false
だった場合にこのメソッドを呼ぶと assert に引っかかるようになっています。
-
時間計算量
先に satisfiable
内で解を計算するので、$O(1)$
参考
- https://people.eecs.berkeley.edu/~satishr/cs270.06/lecture1.pdf
Code
Back to top page