整数和のSATでのエンコード

SATは命題論理式をCNFという標準形で受け取ります(変数かその否定の論理和を論理積でつなげたもの)

使用しているSATライブラリーのminisatではこれを次のように表現します：

1
2
3
4
5
[
    [1, -2, 3],
    [2, 4],
    ...
]

では のような制約をどう表現すればいいでしょうか？
(この変数の和は論理和ではなくtrueなら、falseならとみなしての和を表します)
高機能なソルバーでは標準搭載されていると思いますが、今回使用したライブラリーは低水準のインターフェースしか提供していないようなので自前で実装する必要がありました

これは論理回路をSATで表現して加算器を定義することで実現できます
今回は半加算器(half adder)で用が足りたのでそれのみ示します
の結果を とし繰り上がりを (carry) とすると


が成り立りち(XOR)は論理和・積・否定で表せるので標準形に変換することができます

1
2
3
4
5
6
7
8
9
10
11
12
// x = y + z carry c
export const halfAdder = (c: Var, x: Var, y: Var, z: Var): Cnf => {
  return [
    [-c, y],
    [-c, z],
    [c, -y, -z],
    [-x, -y, -z],
    [-x, y, z],
    [x, -y, z],
    [x, y, -z],
  ];
};

（なおCNFはWolframAlphaで計算できます
https://www.wolframalpha.com/input?i=CNF+of++%28x+equivalent+y+xor+z%29+and+%28c+equivalent+y+and+z%29&lang=ja
）

半加算器ができたので を実装します

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
export const sumEq = (xs: Var[], n: int, newVar: () => Var): Cnf => {
  if (xs.length === 0) {
    if (n === 0) return cnfTrue;
    return cnfFalse;
  }
  if (n === 0) return xs.map(x => [-x]);
  if (n === xs.length) return xs.map(x => [x]);
  if (n < 0 || n > xs.length) return cnfFalse;

  let result: Cnf= [];
  // xsの累積和の最下位ビット
  let t = xs[0];
  let cs: int[] = [];
  for (const x of xs.slice(1)) {
    const c = newVar();
    const v = newVar();
    result = result.concat(halfAdder(c, v, x, t));
    t = v;
    cs.push(c);
  }
  if (n % 2 === 0) {
    result.push([-t]); // t === 0
  } else {
    result.push([t]); // t === 1
  }
  result = result.concat(sumEq(cs, Math.floor(n / 2), newVar));
  return result;
};

同様にも実装できます