Certified Knowledge Compilation with Application to Formally Verified Model Counting

Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad +1

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when form…