制約関数まとめ  
   

制約関数名 パラメータ書式 返り幅(ビット数) 内部制約 内部制約内容/備考 内部制約を逸脱したとき 用途
$Inv $Inv(V) 1 なし Vは、集合ではなく単項であること
$And $And(VEC) 1 なし VEC中すべての要素がtrueであるときtrueを返す
$Or $Or(VEC) 1 なし VEC中、一個でもtrueの要素があるならtrueを返す
$SeqLE $SeqLE(min,max,VEC) max あり VEC中true個数がmin以上max以下の範囲にあること 解なし 主にハード制約
$Onlyone $Onlyone(VEC) なし あり $SeqLEQのmin==1,max==1の特化版 解なし ハード制約のみ
$SeqError $SeqError(min,max,許容エラー数,VEC) 許容エラー数 あり VEC中true個数が(min-許容エラー数、min+許容エラー数の範囲内にあること 解なし ソフト制約
$SeqExpr $SeqExpr(min,max,type,VEC) なし type=0 max以下のときtrueを返す、
type=1:min以上でtrueを返す
type=2のとき、min以上max以下のときtrueを返す
ソフト制約
$EnableGate $EnableGate(control,VEC) VEC幅 なし control端子がtrueのときVECがそのまま返る。control端子がfalseのとき、VEC幅で全てfalseが返る ソフト制約
$SeqComp $SeqComp(VEC1,VEC2) なし ビット幅が異なるとき、大きい方は、大きい幅分だけ0に制約される  解なし 二つの加算機の比較

$SeqErrorは、希望範囲(min-max)から逸脱した分だけtrueが戻ります。しかし、その最大個数は、許容エラー数に制限されます。戻るビット数は、常に許容エラー数個になりますが、希望範囲(min-ma)に収まっている限り、そのtrue個数は、0です。逸脱したビット個数分だけtrueが返ります。この性質は、ソフトエラー数をペナルティとして数えるときに自然な性質になります。すなわち、目標値を超えた分ペナルティとしてカウントする機構を実現したい場合に有用な制約関数になります。

$EnableGateは、名前の通りゲートの役割をします。control端子(1ビット)がtrueのときVECがそのまま素通りして返ります。control端子がfalseのときVEC幅ですべてfalseが返ります。通常、$Enable($SeqExpr.., $SeqError)のように、ソフトエラー数のカウントを場合分けで制御したい場合に使います。

一方、$SeqExprの戻り幅は、要素集合に関係なく常に1ビットです。大きいか、小さいか、ちょうど良いかパラメータtypeに応じて判断することしかできません。目標を超えたら超えた分ペナルティとしてカウントすることはできません。単純に判断の結果を1ビットで返すという仕様です。

$SeqErrorは、内部制約として、許容範囲外を許さないので、制約設計者は、解がないことがないように適切にパラメータ(許容エラー数)を設定する必要があります。$SeqExprに関しては、内部でなんら制約が入っていません。逆に言うと、希望を逸脱しているビット数は、1ビットか数ビットかは区別できません。

1)$Andの図式説明











2)$Orの図式説明













3)$SeqLEの図式説明




4)$SeqErrorの図式説明




5)$SeqExprの図式説明

6)$EnableGateの図式説明


まとめ

  1. 制約は一つづつ書きましょう
  2. 制約は、一つづつ動作を確認しながら、実装しましょう。print文の使用 pythonソースでの確認
  3. ある程度書いたら、ファイルをバックアップして、別ファイルに書くと、後戻りしやすいです。
  4. 外部制約を書いているときは、タイムアウト値は短くでよいです。
  5. 最終解を得るときは、タイムアウト値を長くします。




[Prev] [Next] [Index] [Home]