每当我搜索 2-Sat 的算法时,我都会返回问题决策形式的算法:是否存在满足所有子句的合法值集。但是,这并不能让我轻松找到一组令人满意的布尔值。
如何有效地找到一组满足 2-Sat 实例的合法值?
我正在使用 boost 库在 c++ 中工作,并且希望能够轻松集成代码。
提前致谢
每当我搜索 2-Sat 的算法时,我都会返回问题决策形式的算法:是否存在满足所有子句的合法值集。但是,这并不能让我轻松找到一组令人满意的布尔值。
如何有效地找到一组满足 2-Sat 实例的合法值?
我正在使用 boost 库在 c++ 中工作,并且希望能够轻松集成代码。
提前致谢
如果您有一个决策算法来检测是否存在对 2-SAT 的有效分配,您可以使用它来实际找出实际分配。
首先对整个表达式运行 2-SAT 决策算法。假设它说有一个有效的分配。
现在,如果 x_1 是文字,则将 x_1 分配为 0。现在计算结果表达式的 2-SAT(因此,您将不得不分配一些其他文字,例如,如果出现 x_1 OR x_3,您还需要设置 x_3到 1)。
如果结果表达式是 2-Satisfiable,那么您可以将 x_1 设为 0,否则将 x_1 设为 1。
现在您可以找到有关每个文字的信息。
对于更有效的算法,我建议您尝试使用蕴含图方法。
你可以在这里找到更多信息:http ://en.wikipedia.org/wiki/2-satisfiability
相关部分:
一个 2-satisfiability 实例是可解的,当且仅当实例的每个变量都属于隐含图的不同强连通分量而不是同一变量的否定。由于基于深度优先搜索的算法可以在线性时间内找到强连通分量,因此相同的线性时间界限也适用于 2 可满足性。
每个强连通分量中的文字要么全为零,要么全为 1。
至少有一种算法列出了 2-sat 问题的所有解决方案,作者是 Tomas Feder:http ://www.springerlink.com/content/j582276p06276l12/