如何在 SAT 求解器中构造文字答案

【问题标题】：How to construct literals in SAT solvers如何在 SAT 求解器中构造文字
【发布时间】：2016-02-23 02:04:30
【问题描述】：

我正在研究minisat的源码，这里有一个follow inline函数

 typedef int Var;
 inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }

which recibes 作为输入一个整数 var（DIMAC 文件的一个整数）并返回一个文字 p，我不明白为什么 var 加上 var 然后加上符号？你能帮忙理解一下吗？

【问题讨论】：

标签： solver sat

【解决方案1】：

假设p.x 只是一个常规整数，似乎正在发生的事情是var 映射到2*var，如果sign 为假，2*var + 1，如果sign 为真.大概这样做的目的是，在文字中，p.x % 2 将告诉您var 是否对应于否定或非否定变量，偶数p.x 对应于否定变量，奇数p.x 对应于非- 否定变量。原始的var 很容易被p.x/2 恢复。此函数允许您将 (int,bool) 对编码为单个 int。

【讨论】：

谢谢约翰，但我在 minisat 资源中寻找这个表达式“p.x/2”，但我没有找到这个
无论表达式p.x/2 是否出现在源代码中，事实上var 和sign 都可以从p 中恢复，因为它产生了您提供的代码偶数或奇数 int 取决于 sign 的值。也许代码以后不需要恢复var（尽管这似乎不太可能），也许它使用了移位运算符，也许它在代码的其他部分中使用了p以外的标识符，例如可能是数组的一部分，而不是单独的 Lit 值。