Counting for Satisfiability by Inverting Resolution

摘要

We present a new algorithm for counting truth assignments of a clausal formula using inverse propositional resolution and its associated normalization rules. The idea is opposite of the classical resolution, and is achieved by constructing in a bottom-up manner a computation graph. This means that we successively add complementary literals to generate new bigger clauses instead of solving them. Next, we make a comparison between the classical and inverse resolution, followed by a new algorithm which combines these two techniques for solving the SAT problem.