0

私はミニサットのソースを研究していますが、ここにはフォローインライン機能があります

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

入力として整数 var (DIMAC ファイルの整数) を受け取り、リテラル p を返します。なぜ var に var が追加され、次に符号が追加されるのかわかりません。それを理解するのを手伝ってくれませんか？

4

1 に答える 1

0

それが単なる通常の int であると仮定すると、p.x起こっているように見えるのは、が false の場合と が true の場合のvarいずれかにマップされることです。おそらく、これの目的は、リテラルでは、否定変数または非否定変数に対応するかどうかを示し、偶数は否定変数に対応し、奇数は非否定変数に対応することです。オリジナルは によって簡単に復元されます。この関数を使用すると、(int,bool) ペアを単一の int としてコーディングできます。2*varsign2*var + 1signp.x % 2varp.xp.xvarp.x/2

于 2016-02-22T18:04:30.293 に答える