### 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.