arXivDaily arXiv每日学术速递 周一至周五更新
arXiv cs/0610174cs.DScs.CCcs.LO
收藏

带参数关联树宽的# SAT的固定参数算法

A Fixed-Parameter Algorithm for #SAT with Parameter Incidence Treewidth

Marko Samer, Stefan Szeider

摘要:

我们提出了一种有效的固定参数算法,用于#SAT,由关联树宽度参数化,即,二分图的树宽,其顶点是给定CNF公式的变量和子句;当且仅当变量出现在子句中时,变量和子句通过边连接。我们的算法运行时间为O(4^kklN),其中k表示关联树宽度,l表示最大子句的大小,N表示树分解的节点数。

英文摘要:

We present an efficient fixed-parameter algorithm for #SAT parameterized by the incidence treewidth, i.e., the treewidth of the bipartite graph whose vertices are the variables and clauses of the given CNF formula; a variable and a clause are joined by an edge if and only if the variable occurs in the clause. Our algorithm runs in time O(4^k k l N), where k denotes the incidence treewidth, l denotes the size of a largest clause, and N denotes the number of nodes of the tree-decomposition.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑