Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width

• Autorzy: Ganian R. , Hlinĕný P. , Obdržálek J.
• Języki publikacji: EN

Abstrakty

EN

We provide a parameterized algorithm for the propositional model counting problem #SAT, the runtime of which has a single-exponential dependency on the rank-width of the signed graph of a formula. That is, our algorithm runs in time O(t³ · 2^3t(t+1)/2 ·|φ| for a width-t rankdecomposition of the input φ, and can be of practical interest for small values of rank-width. Previously, analogical algorithms have been known – e.g. [Fischer, Makowsky, and Ravve] – with a single-exponential dependency on the clique-width k of the signed graph of a formula with a given k-expression. Our algorithm presents an exponential runtime improvement over the worst-case scenario of the previous one, since clique-width reaches up to exponentially higher values than rankwidth. We also provide an algorithm for the MAX-SAT problem along the same lines.

Słowa kluczowe

EN

propositional model counting; satisfiability; rank-width; clique-width; parameterized complexity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 123, nr 1
• Strony: 59--76
• Opis fizyczny: Bibliogr. 24 poz., wykr.

Twórcy

autor

Ganian R.

• Faculty of Informatics Masaryk University Botanická 68a, Brno, Czech Republic

autor

Hlinĕný P.

• Faculty of Informatics Masaryk University Botanická 68a, Brno, Czech Republic

autor

Obdržálek J.

• Faculty of Informatics Masaryk University Botanická 68a, Brno, Czech Republic

Bibliografia

• [1] Alon, N., Gutin, G., Kim, E. J., Szeider, S., Yeo, A.: Solving MAX-r-SAT Above a Tight Lower Bound, Algorithmica, 61(3), 2011, 638–655.
• [2] Arora, S., Safra, S.: Probabilistic checking of proofs: A new characterization of NP, J. ACM, 45, 1998, 70–122.
• [3] Bodlaender, H.: Treewidth: Algorithmic Techniques and Results, MFCS’97, 1295, Springer, 1997.
• [4] Bui-Xuan, B.-M., Telle, J. A., Vatshelle,M.: H-join decomposable graphs and algorithmswith runtime single exponential in rankwidth, Discrete Appl. Math., 158(7), 2010, 809–819.
• [5] Chen, J., Kanj, I. A.: Improved exact algorithms forMAX-SAT, Discrete Appl.Math., 142(1-3), 2004, 17–27.
• [6] Corneil, D., Rotics, U.: On the relationship between cliquewidth and treewidth, SIAM J. Comput., 34(4), 2005, 825–847.
• [7] Courcelle, B., Kanté,M.: Graph Operations Characterizing Rank-Width, Discrete Appl.Math., 157(4), 2009, 627–640.
• [8] Courcelle, B., Makowsky, J. A., Rotics, U.: Linear Time Solvable Optimization Problems on Graphs of Bounded Clique-Width., Theory Comput. Syst., 33(2), 2000, 125–150.
• [9] Fischer, E., Makowsky, J. A., Ravve, E.: Counting truth assignments of formulas of bounded tree-width or clique-width, Discrete Appl. Math., 156, 2008, 511–529.
• [10] Ganian, R., Hlinˇený, P.: On Parse Trees and Myhill–Nerode–type Tools for handling Graphs of Bounded Rank-width, Discrete Appl. Math., 158, 2010, 851–867.
• [11] Georgiou, K., Papakonstantinou, P.: Complexity and algorithms for well-structured k-SAT instances, SAT’08, 4996, Springer, 2008.
• [12] Goldman, J., Rota, G.-C.: The number of subspaces of a vector space, in: Recent Progress in Combinatorics (W. T. Tutte, Ed.), Academic Press, 1969, 75–83.
• [13] Hlinĕný, P.: A Parametrized Algorithm for Matroid Branch-Width, SIAM J. Comput., 35(2), 2005, 259–277.
• [14] Hlinĕný, P., Oum, S.: Finding Branch-decomposition and Rank-decomposition, SIAM J. Comput., 38, 2008, 1012–1032.
• [15] Kanté, M.: The Rank-Width of Directed Graphs, arXiv:0709.1433v3,March 2008.
• [16] Kanté, M., Rao, M.: The Rank-Width of Edge-Colored Graphs, Theory of Computing Systems: http://link.springer.com/article/10.1007%2Fs00224-012-9399-y.
• [17] Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of Acyclic and Almost Acyclic CNF Formulas, FSTTCS 2010, 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, ISBN 978-3-939897-23-1.
• [18] Oum, S.: Rank-width and vertex-minors, J. Comb. Theory Ser. B, 95(1), 2005, 79–100.
• [19] Oum, S.: Approximating rank-width and clique-width quickly, ACM Trans. Algorithms, 5(1), 2008, 1–20, ISSN 1549-6325.
• [20] Oum, S.: Rank-width is less than or equal to branch-width, J. Graph Theory, 57(3), 2008, 239–244.
• [21] Oum, S., Seymour, P. D.: Approximating clique-width and branch-width, J. Combin. Theory Ser. B, 96(4), 2006, 514–528.
• [22] Razgon, I., O’Sullivan, B.: Almost 2-SAT is fixed-parameter tractable, J. Comput. System Sci., 75(8), 2009, 435–450.
• [23] Samer, M., Szeider, S.: Algorithms for propositional model counting, J. Discrete Alg., 8, 2010, 50–64.
• [24] Valiant, L. G.: The complexity of computing the permanent, Theoret. Comput. Sci., 8(2), 1979, 189–201