Improving MCS Enumeration via Caching: MCS列挙において、見つかったunsat coreの情報を保存しておいて、 その上位集合である場合にはSATソルバ呼び出しを省くことで高速化という話。 BがA1,…Anのいずれかの上位集合であることは、要素を変数と同一視すると ∨¬A1 ∧ … ∧ ∨¬A1 ∧ ∧B の充足不能になるのでSATソルバで実現。
ただ、利点と欠点の両方があるとは思うけれど、別のSATソルバインスタンスではなく元の問題を持っているSATソルバインスタンスの方に直接unsat coreをブロックするような節を追加してしまうという方法もあると思うし、それであれば既存の試みがないのかなぁ。 自分も Max-SAT / PBO / WBO のアルゴリズムの実装の方ではそういう実装をしてたことがあるので……
あと、SATソルバを一種のデータベースとして使う発想は、MARCO[2]にも通じるものがあるような気がするなと思った。対象としている問題も近いし。
[1] A. Previti, C. Mencía, M. Järvisalo, and J. Marques-Silva, "Improving MCS enumeration via caching," in Theory and Applications of Satisfiability Testing – SAT 2017, ser. Lecture Notes in Computer Science, S. Gaspers and T. Walsh, Eds. Springer International Publishing, 2017, vol. 10491, pp. 184-194.
https://link.springer.com/chapter/10.1007/978-3-319-66263-3_12
https://www.cs.helsinki.fi/u/mjarvisa/papers/pmjm.sat17.pdf
[2] M. Liffiton and A. Malik, "Enumerating infeasibility: Finding multiple MUSes quickly," in Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, C. Gomes and M. Sellmann, Eds. pp. 160-175.
https://link.springer.com/chapter/10.1007/978-3-642-38171-3_11
http://sun.iwu.edu/~mliffito/publications/cpaior13_liffiton_MARCO.pdf
参考: https://plus.google.com/+MasahiroSakai/posts/3TE69gnMKJK
Improving MCS Enumeration via Caching
