Although several tractable classes of SAT are known, none of these turns out to be easy for optimization, probabilistic and counting versions of SAT. These problems can be solved efficiently for formulas with bounded treewidth. However, the resulting time bounds are exponential in the treewidth, which means exponential in the size of the largest clause. In this paper we show that solution methods for formulas with treewidth two can be combined with specialized techniques for dealing with "long" clauses, thus obtaining time bounds independent of the treewidth. This leads to the definition of a new class of tractable instances for SAT and its extensions. This class is related to a particular class of reducible hypergraphs, that extends partial 2-trees and hypertrees.
展开▼
