General plans for counting satisfying assignments.
More...
Go to the source code of this file.
Detailed Description
General plans for counting satisfying assignments.
 Todo:
 Create milestones.
 Todo:
 Write the direct algorithm (running through all total assignments)

Perhaps in "Counting/Basics.mac".
 Todo:
 Write a scheme which uses r_ksplitting trees
 Todo:
 okltest_satprob

We should perhaps create Counting/tests/Basics.mac, and move this general testfunction there.

DONE This testfunction should be a general test function for the counting of satisfiying assignments of boolean clausesets.
 Todo:
 satprob_mcind
 Todo:
 satprob_incexl_hitting

Similar to satprob_mcind, compute approximations.

One would assume, that this computation is always less efficient than satprob_mcind?
 Todo:
 Connect to the countingmodule in part Satisfiability.
 Todo:
 Sumproduct (belief propagation) and beyond

Implement the sumproduct algorithm (see also Satisfiability/Algorithms/SumProduct/plans/general.hpp).

Implement the "Iterative JoinGraph Propagation" IJGP, especially in the form "IJGP(i)SC" from [Kask, Dechter, Gogate; CountingBased LookAhead Schemes for Constraint Satisfaction; CP 2004].

Comparing tw(vig(F)) (the treewidth of the variableinteraction graph) with alpha(cg(F)) (the independence number of the conflict graph) is here of interest.
 Todo:
 Sampling falsifying assignments

In Section 28.1 of [Vazirani, 2001, Approximation Algorithms] one finds an algorithm for efficient sampling of falsifying assignments for CNF (an "FPRAS"; there in the language of DNF).

This is an easy algorithm, and we should implement it. Search also for some other literature.

Augmented with the calculations on how often to sample to achieve some guarantee, that is, for given approximation ratio epsilon and success probability p, find a way (by random sampling and repeating the whole computation) to achieve (epsilon,p) as efficient as possible.
Definition in file general.hpp.