自作SATソルバのSMTソルバ実装用のフックのテストのために、SAT modulo SAT的なものを試した https://github.com/msakai/toysolver/commit/e610aa6ddc4820424c8ff1cdcb67f1119b9650e6 のだけれど、そういえば Continuation Fest 2008 (継続祭り) http://logic.cs.tsukuba.ac.jp/Continuation/ の際に Chung-chieh Shan さんと、SAT modulo SAT みたいな話をしたのをふと思い出した。