sunasunaxの日記

制約論理プログラム iZ-C の紹介

論理的関係制約を制約論理プログラム iZ-Cを使って表現します。

論理的関係制約を制約論理プログラム iZ-Cを使って表現します。
-------------------------------------------------------------------------------------
制約変数xiが{1,0}である場合、論理関数は次のように制約を設定することができます。

 

NOT                  cs_EQ(cs_ReifEQ(x1, 0), 1);

 

AND                  cs_EQ(cs_Add(3, x1, x2, x3), 3);

 

OR                    cs_NEQ(cs_Add(3, x1, x2, x3), 0);

 

EXOR                y1 = cs_ReifEQ(cs_Add(3, x1, x2, x3), 1);
                          y2 = cs_ReifEQ(cs_Add(3, x1, x2, x3), 3);
                          cs_NEQ(cs_Add(y1, y2), 0);

 

全称記号∀          cs_EQ(cs_Add(3, x1, x2, x3), 3);

 

存在記号∃          cs_NEQ(cs_Add(3, x1, x2, x3), 0);