Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas.
SMTで、スケルトン(boolean abstraction 結果の命題論理式)を、普通のSATソルバで解くと、完全な割当を計算してしまうので、原子論理式の真偽判定のコストが大きような理論だと嬉しくない。 そこで、dual-rail encoding + 最適化(PBO, partial Max-SAT, etc.) で minimum implicant を求めて、最小な部分割当を計算することで、不要な原子論理式の真偽判定を省こうという話。
発想としては自然なんだけど、そのまま適用できる背景理論は限られそう。 例として Software Performance Logic (SPL) を出しているけれど、これは原子論理式の真偽判定のコストが大きい一方で、原子論理式の組み合わせによって矛盾が発生することがないという意味で、非常に特殊な背景理論のはず。 一般的な背景理論では、スケルトンに対する充足部分割当に含まれない原子論理式についても、背景理論に関して整合的な真偽割当が可能かを、何らかの形で検査しないといけない。
https://link.springer.com/chapter/10.1007/978-3-319-00948-3_15
http://ktiml.mff.cuni.cz/~balyo/papers/sera2013.pdf