Pair Constraints Domain Propagation

 ペア制約には二つあります。Inhibit とImplicationです。今、ペア禁止制約で、初期に片方が予定等によりハードFixしている場合を考えます。Inhibitの場合、

assert(!(A&B));ですから

assert(!A|!B)；となり、

今AがFixしている状態を考えると

if (!A) then !A|!B becomes to be satisfactory regardless of the state B.

else !B must be True;

となります。特に、BがORオペレータだったりすると、A=Trueの場合；

assert(!B)=assert(!(B0|B1|B2...))=assert(!B0& !B1&B2...);であるので全BスタッフがFalseであることを強いられます。

Aは、初期からFIXしているので、Aの状態によっては、Bの状態をFIXさせる必要があります。Implication(A→B)も同様に考えることが出来ます。

このように、片方がFIXしている場合、自動的に満足する、あるいは、もう片方が満足することを強いられることが起こります。これがDomain　Propagationです。

＜Branching　Domain　Propagation＞

初期だけではなく、Branchingによっても、同様の事は起こります。新しいBranching　Nodeが発生する都度に、それによるDomain Propagationが発生し再度計算しなおす必要があります。Domain　Propagationは、MIPソルバのBranchingでも活用されています。特に、infeasibleを検出するのがlinear solverは、苦手なので(というよりも線形ソルバと離散領域の本質的な違いに起因する）、その場面で効果がある模様です。

Hybrid Branching (zib.de)

<Domain Propagationの実装>

上記は、簡単な例でしたが、一般には、＜＝等の不等式の制約も入ってきて一般化は複雑です。

面倒なことは全てSAT　Solverに任せ、Solveで済ませてしまおうというのが私の発想です。Domain Propagationは、SAT SolverのUnit Propagationです。なのでUnit PropagationによりFixしている項を取り出せれば十分であり、SAT Solver自体はBlack　Boxとして扱えます。

が強いられることになります。これがDomain Propagationです。ペア制約があると、各スタッフ間は、