Please use this identifier to cite or link to this item:
https://doi.org/10.1007/s10462-004-4329-2
Title: | Counting for satisfiability by inverting resolution | Authors: | Andrei, S. | Keywords: | Algorithms Counting truth assignments Satisfiability |
Issue Date: | Dec-2004 | Citation: | Andrei, S. (2004-12). Counting for satisfiability by inverting resolution. Artificial Intelligence Review 22 (4) : 339-366. ScholarBank@NUS Repository. https://doi.org/10.1007/s10462-004-4329-2 | Abstract: | We present a new algorithm for counting truth assignments of a clausal formula using inverse prepositional 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. | Source Title: | Artificial Intelligence Review | URI: | http://scholarbank.nus.edu.sg/handle/10635/114631 | ISSN: | 02692821 | DOI: | 10.1007/s10462-004-4329-2 |
Appears in Collections: | Staff Publications |
Show full item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.