solver - 如何在 SAT 求解器中构造文字

Question

我正在研究 minisat 的来源，这里有一个跟随内联函数

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

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

Answer 1

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