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.

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.