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

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. 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 2013
Type Article in Periodical
Magazine / Source Fundamenta Informaticae
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.3233/FI-2013-800
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.

More info