Proof systems for #SAT

November 18, 2019

Florent Capelli (Université de Lille)

In this talk, we will show how one can augment classes of Boolean
circuits used in knowledge compilation so that one can efficiently check that
they are equivalent to a given CNF formula. We will show that it can be applied
to define Cook-Reckhow proof systems for #SAT and maxSAT and how one can use
this idea to output certificates from existing tools solving #SAT.