The parsimonious Cook–Levin theorem

The Cook–Levin reduction is polynomial-time (computableInPolyTime_reduce) and parsimonious (modelCount_reduce): applied to the verifier of a function f in #P, it maps an instance a to a formula with exactly f a satisfying assignments. Together with SharpSAT.mem_SharpP, this proves that #SAT is #P-complete under parsimonious polynomial-time reductions Valiant, Papadimitriou, Chapter 18.

The count is exact: #P counts the certificates of exactly the verifier's length, the tableau has one variable for each of their bits, and all its other variables are determined by them.

Main results

• Cslib.Complexity.CookLevin.SharpSAT_sharpPHard: every function in #P reduces parsimoniously to #SAT.
• Cslib.Complexity.CookLevin.SharpSAT_sharpPComplete: #SAT is #P-complete.

References

• L. Valiant, The complexity of computing the permanent
• C. H. Papadimitriou, Computational Complexity, Chapter 18.
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 17.3.

theorem Cslib.Complexity.CookLevin.SharpSAT_sharpPHard : SharpPHard encCNF SharpSAT

The parsimonious Cook–Levin theorem: every function in #P reduces parsimoniously to #SAT, through the tableau of its verifier.

theorem Cslib.Complexity.CookLevin.SharpSAT_sharpPComplete : SharpPComplete encCNF SharpSAT

#SAT is #P-complete under parsimonious polynomial-time reductions.