Differentiable SAT/ASP

We propose Differentiable SAT and Differentiable Answer Set Programming for multi-model optimization through gradient-controlled answer set or satisfying assignment computation. As a use case, we also show how our approach can be used for expressive probabilistic inference constrained by logical background knowledge. In addition to presenting an enhancement of the CDNL/CDCL algorithm as primary implementation approach, we introduce alternative algorithms which use an unmodified ASP solver and map the optimization task to conventional answer set optimization or use so-called propagators.