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.
Hypergraph Reductions and Satisfiability Problems / Pretolani, Daniele. - STAMPA. - 2919:(2004), pp. 383-397. (Intervento presentato al convegno 6th International Conference on Theory and Applications of Satisfiability Testing tenutosi a Santa Margherita Ligure, ITALY nel MAY 05-08, 2003) [10.1007/978-3-540-24605-3_29].
Hypergraph Reductions and Satisfiability Problems
PRETOLANI, Daniele
2004
Abstract
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.
Pubblicazioni consigliate
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris
