Arrow Research search

Author name cluster

Daniel Fremont

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

AAAI Conference 2017 Conference Paper

Maximum Model Counting

  • Daniel Fremont
  • Markus Rabe
  • Sanjit Seshia

We introduce the problem Max#SAT, an extension of model counting (#SAT). Given a formula over sets of variables X, Y, and Z, the Max#SAT problem is to maximize over the variables X the number of assignments to Y that can be extended to a solution with some assignment to Z. We demonstrate that Max#SAT has applications in many areas, showing how it can be used to solve problems in probabilistic inference (marginal MAP), planning, program synthesis, and quantitative information flow analysis. We also give an algorithm which by making only polynomially many calls to an NP oracle can approximate the maximum count to within any desired multiplicative error. The NP queries needed are relatively simple, arising from recent practical approximate model counting and sampling algorithms, which allows our technique to be effectively implemented with a SAT solver. Through several experiments we show that our approach can be successfully applied to interesting problems.

PDF Details

AAAI Conference 2014 Conference Paper

Distribution-Aware Sampling and Weighted Model Counting for SAT

  • Supratik Chakraborty
  • Daniel Fremont
  • Kuldeep Meel
  • Sanjit Seshia
  • Moshe Vardi

Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distribution-aware sampling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inherent complexity of the exact versions of the problems, interest has focused on solving them approximately. Prior work in this area scaled only to small problems in practice, or failed to provide strong theoretical guarantees, or employed a computationally-expensive most-probable-explanation (MPE) queries that assumes prior knowledge of a factored representation of the weight distribution. We identify a novel parameter, tilt, which is the ratio of the maximum weight of satisfying assignment to minimum weight of satisfying assignment and present a novel approach that works with a black-box oracle for weights of assignments and requires only an NP-oracle (in practice, a SAT-solver) to solve both the counting and sampling problems when the tilt is small. Our approach provides strong theoretical guarantees, and scales to problems involving several thousand variables. We also show that the assumption of small tilt can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known.

PDF Details
v2026.09.13