设计HCP的SAT
摘要：对于任意的无向图$G$，我们使用布尔代数工具来设计满足性问题（SAT）来解决哈密顿环问题（HCP）。所得到的SAT是关于哈密顿环存在条件的逻辑表达式，并且使用$m$个布尔变量，其中$m$是图的边数。这个布尔表达式当且仅当初始图是哈密顿图时为真。也就是说，布尔变量的每个满足赋值确定了$G$的一个哈密顿环，而$G$的每个哈密顿环又对应于布尔变量的一个满足赋值。在一般情况下，所得到的布尔表达式可能会有指数长度（布尔文字的数量）。
作者：Anatoly D. Plotnikov (Vinnitsa Institute of Regional Economics and Management)
论文ID：cs/9903006
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23