Pith. sign in

REVIEW 1 cited by

Understanding model counting for $\beta$-acyclic CNF-formulas

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1405.6043 v1 pith:QLZ35MMY submitted 2014-05-23 cs.CC cs.AI

classification cs.CCcs.AI
keywords algorithmacyclicbetamathrmdynamicprogrammingalgorithmsalong
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
abstract

We extend the knowledge about so-called structural restrictions of $\mathrm{\#SAT}$ by giving a polynomial time algorithm for $\beta$-acyclic $\mathrm{\#SAT}$. In contrast to previous algorithms in the area, our algorithm does not proceed by dynamic programming but works along an elimination order, solving a weighted version of constraint satisfaction. Moreover, we give evidence that this deviation from more standard algorithm is not a coincidence, but that there is likely no dynamic programming algorithm of the usual style for $\beta$-acyclic $\mathrm{\#SAT}$.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. On Symbolic Approaches for Computing the Matrix Permanent

    cs.DS 2019-08 conditional novelty 6.0 of 10

    An ADD-based symbolic Ryser algorithm computes permanents of dense and similar-row matrices up to size 70-80, outperforming CNF-based exact counters and explicit Ryser on these instances.

Pith tools