The Relative Strength of #SAT Proof Systems

Area of Science:

• Computational complexity theory
• Automated reasoning
• Knowledge representation

Background:

• The #SAT problem involves counting satisfying assignments for propositional formulas.
• Four proof systems (kcps, MICE, CPOG, CLIP) were introduced to model #SAT solving and enable proof logging.
• CLIP was known to simulate the other three systems, but their interrelations were unclear.

Purpose of the Study:

• To completely determine the simulation order of the four #SAT proof systems: kcps, MICE, CPOG, and CLIP.
• To clarify the proof complexity relationships between these systems.
• To establish the relative strengths of these #SAT proof systems.

Main Methods:

• Theoretical analysis of proof system simulations.
• Establishing simulation and incompressibility results between systems.
• Comparative analysis of proof complexity.

Main Results:

• The simulation order is established: CPOG simulates both MICE and kcps.
• MICE and kcps are shown to be exponentially incomparable.
• CLIP simulates all other systems, but its relationship to them in terms of strict simulation is not detailed here.

Conclusions:

• CPOG is strictly stronger than MICE and kcps.
• The established order provides a comprehensive understanding of the proof complexity landscape for these #SAT solvers.
• This work resolves open questions regarding the relationships between these important #SAT proof systems.