Please use this identifier to cite or link to this item: https://doi.org/10.1109/SYNASC.2009.12
Title: A hierarchy of tractable subclasses for SAT and counting SAT problems
Authors: Andrei, Ş.
Grigoraş, G.
Rinard, M.
Chuan Yap, R.H. 
Issue Date: 2009
Source: Andrei, Ş., Grigoraş, G., Rinard, M., Chuan Yap, R.H. (2009). A hierarchy of tractable subclasses for SAT and counting SAT problems. SYNASC 2009 - 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing : 61-68. ScholarBank@NUS Repository. https://doi.org/10.1109/SYNASC.2009.12
Abstract: Finding subclasses of formulæ for which the SAT problem can be solved in polynomial time has been an important problem in computer science. We present a new hierarchy of propositional formulæ subclasses for which the SAT and counting SAT problems can be solved in polynomial time. Our tractable subclasses are those propositional formulæ in conjunctive normal form where any set of k + 1 clauses are related, i.e., there exists at least one literal in one clause that appears negated in another clause of the considered set of k + 1 clauses. We say this subclass of formulæ is of rank k and it is different from previously known subclasses that are solvable in polynomial time. This is an improvement over the SAT Dichotomy Theorem and the counting SAT Dichotomy Theorem, since our subclass can be moved out from the ℕℙ-complete class to the ℙ class. The membership problem for this new subclass can be solved in O(n · l k+1), where n, l and k are the number of variables, clauses and the rank (1 ≤ k ≤ l - 1), respectively. We give an efficient algorithm to approximate the number of assignments for any arbitrary conjunctive normal form propositional formula by an upper bound. © 2009 IEEE.
Source Title: SYNASC 2009 - 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
URI: http://scholarbank.nus.edu.sg/handle/10635/39934
ISBN: 9780769539645
DOI: 10.1109/SYNASC.2009.12
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

1
checked on Dec 14, 2017

WEB OF SCIENCETM
Citations

1
checked on Nov 20, 2017

Page view(s)

62
checked on Dec 17, 2017

Google ScholarTM

Check

Altmetric


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