On Tackling the Limits of Resolution in SAT Solving: CDCL SATソルバによる充足不能性の証明は、導出原理(resolution)による証明だけど、resolutionはproof complexity的にはあまり強力ではなく、例えば鳩ノ巣原理(m個の巣にm+1の鳩を入れることを表す命題論理式の充足不能性)の証明は指数サイズの証明になり、SATソルバでは全然スケールしない。 それに対して、dual-railエンコーディングでHormMaxSATに帰着すると、Max-SAT Resolution や core-guided Max-SAT の一種で(元の論理式の充足不能性に相当するboundの)多項式サイズの導出が存在し、実装でも性能が出たよというような話。 元になったソルバの話をよく知らないこともあり、実装の話はあまり理解できておらず。
https://link.springer.com/chapter/10.1007/978-3-319-66263-3_11
https://arxiv.org/abs/1705.01477
On Tackling the Limits of Resolution in SAT Solving
