Paper by Erik D. Demaine

Reference:

MIT Hardness Group, Josh Brunner, Erik D. Demaine, Jenny Diomidova, Timothy Gomez, Markus Hecher, Frederick Stock, and Zixiang Zhou, “Easier Ways to Prove Counting Hard: A Dichotomy for Generalized #SAT, Applied to Constraint Graphs”, in Proceedings of the 35th International Symposium on Algorithms and Computation (ISAAC 2024), LIPIcs, volume 322, Sydney, Australia, December 8–11, 2024, 51:1–51:14.

BibTeX

@InProceedings{SharpSAT_ISAAC2024,
  key           = {MIT},
  AUTHOR        = {{MIT Hardness Group} and Josh Brunner and Erik D. Demaine and Jenny Diomidova and Timothy Gomez and Markus Hecher and Frederick Stock and Zixiang Zhou},
  TITLE         = {Easier Ways to Prove Counting Hard: A Dichotomy for Generalized {\#SAT}, Applied to Constraint Graphs},
  BOOKTITLE     = {Proceedings of the 35th International Symposium on Algorithms and Computation (ISAAC 2024)},
  bookurl       = {https://sites.google.com/view/isaac2024/home},
  ADDRESS       = {Sydney, Australia},
  SERIES        = {LIPIcs},
  VOLUME        = 322,
  MONTH         = {December 8--11},
  YEAR          = 2024,
  PAGES         = {51:1--51:14},

  length        = {14 pages},
  withstudent   = 1,
  doi           = {https://dx.doi.org/10.4230/LIPIcs.ISAAC.2024.51},
  dblp          = {https://dblp.org/rec/conf/isaac/GroupBDDGHSZ24},
  comments      = {This paper is also available from <A HREF="https://doi.org/10.4230/LIPIcs.ISAAC.2024.51">LIPIcs</A>.},
}

Abstract:

To prove #P-hardness, a single-call reduction from #2SAT needs a clause gadget to have exactly the same number of solutions for all satisfying assignments — no matter how many and which literals satisfy the clause. In this paper, we relax this condition, making it easier to find #P-hardness reductions. Specifically, we introduce a framework called Generalized #SAT where each clause contributes a term to the total count of solutions based on a given function of the literals. For two-variable clauses (a natural generalization of #2SAT), we prove a dichotomy theorem characterizing when Generalized #SAT is in FP versus #P-complete.

Equipped with these tools, we analyze the complexity of counting solutions to Constraint Graph Satisfiability (CGS), a framework previously used to prove NP-hardness (and PSPACE-hardness) of many puzzles and games. We prove CGS ASP-hard, meaning that there is a parsimonious reduction (with algorithmic bijection on solutions) from every NP search problem, which implies #P-completeness. Then we analyze CGS restricted to various subsets of features (vertex and edge types), and prove most of them either easy (in FP) or hard (#P-complete). Most of our results also apply to planar constraint graphs. CGS is thus a second powerful framework for proving problems #P-hard, with reductions requiring very few gadgets.

Comments:

This paper is also available from LIPIcs.

Length:

The paper is 14 pages.

Availability:

The paper is available in PDF (741k).

See information on file formats.

[Google Scholar search]