Better algorithms for satisfiability problems for formulas of bounded rank-width

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

GANIAN Robert HLINĚNÝ Petr OBDRŽÁLEK Jan

Year of publication 2010
Type Article in Proceedings
Conference IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
MU Faculty or unit

Faculty of Informatics

Citation
Web
Doi http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.73
Field Informatics
Keywords propositional model counting; satisfiability; rank-width; clique-width; parameterized complexity
Description We provide a parameterized polynomial algorithm for the propositional model counting problem #SAT, the runtime of which is single-exponential in the rank-width of a formula. Previously, analogous algorithms have been known -- e.g.~[Fischer, Makowsky, and Ravve] -- with a single-exponential dependency on the clique-width of a formula. Our algorithm thus presents an exponential runtime improvement (since clique-width reaches up to exponentially higher values than rank-width), and can be of practical interest for small values of rank-width. We also provide an algorithm for the MAX-SAT problem along the same lines.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.