Heuristic Planning with SAT: Beyond Uninformed Depth-First Search(Rintanen; 2010)
RintanenさんのPlanningをSATソルバを使って解く一連の論文の2010のもの
Planning-specificなheuristicをSATソルバに入れることで、satソルバの探索を効率的に行うというもので、Rintanen 2011で構築されたプランナM, Mpに取り込まれている技術のうちの一つである。
Conflict Driven Clause Learning(CDCL)に深さ優先探索をさせるように変更したもの(時期的にはChaffの改造だろうか?2010の別のRintanen氏の論文で記述があるそうだ)が当時のプランニング用のSATソルバの最先端だったそうだが、さらに一方踏み込んで、ソルバの変数選択や、値の割当てのヒューリスティックとして、プランニングの知識を入れようとしている。
よく知られたプランニングをモデル化した際のソルバ側の探索ヒューリスティックとしては、命題変数とアクション変数が存在するが、全てのアクション変数の割当が決定すると命題変数の値は一意に定まるため、アクション変数に優先的に(あるいはアクション変数のみに)値を割り当てる、というものがある。 このような割当てを実現する方法として(僕が知っているの)は、
- この論文では帰着先のモデルとしてSATを利用しているが、どのモデルでも通用するのはソルバを改造(または実装)することである
- しかしながら、できれば汎用ソルバをそのまま使って性能が出るに越したことはないと思う
- IP(MIP)を使う場合には、探索の際に決定変数になるのは整数制約の付いている変数であることに着目して、関数的に決定される変数が整数変数によって抑えられるように制約を加え、その上で連続変数とすることで割当順序の操作が可能である
- CPの場合には、多くのソルバでドメインが小さい変数から決定変数として採用されるという汎用ヒューリスティックが採用されるのでそうなるようにモデルを工夫して設計するか、またはソルバにヒントを与える仕組みがMinizincという中間言語で導入されているのでこれを利用することが考えられる
この論文で提案されている変数選択、値の割当ての際のヒューリスティックは上に挙げたような自明なものよりももう一歩踏み込んだもので、この実現のために、SATソルバにRintanen氏は手を加えているようである。 具体的なヒューリスティックとしては、後ろ向き推論のようなことを実現するための仕組みを提案している。
これは * ゴール命題(top-level goal)は最終的に真となる必要がある * するとゴール命題を真とするようなアクションが実行される必要がある * すると今度はそのアクションの前提条件(subgoalと呼んでいる)がその前に真になっている必要がある
というのを繰り返しながら、必要度の高そうな変数から割当てを行うというものである。 さらなる工夫として、goalの未割当てであるような深さをプライオリティーとしてプライオリティーキューを構築することで、ゴールに近いんだがまだ真になっていないような命題から割当てを行うような工夫もしている。 ここでは、subgoalの必要度の高さをtop-level goalから何回目の展開で現れたsubgoalか、で見積もり、より必要そうなsubgoalから順に割当てを行うような工夫もありうるのではないだろうかと思う。
もう一つ、actionからsubgoalを生成する際に、最初に見つけたものを採用するのではなく、N個ののsubgoalを見つけ、その中から一つ適当に引く、ということをしている。 ただし、素朴にこれを行うと、以前に展開した残りがその後の探索の邪魔をすることがあり、N=2よりも大きいと性能が上がらなかったそうである。 ここで、time-stampという概念を導入し、展開した残り物がqueueにたくさん入ってきたら展開を打ち切る、ということをすると、最もよい結果が出たそうである。
より具体的なアルゴリズムと性能評価は論文に譲ることとする。
メモ: * Rintanen;2011とExperimental Resultsの様子がだいぶ変わっている。 * IPC1998, 2008のドメインがいくらか追加されている * その結果、この論文ではM > LAMAだったのが2011の論文では逆転している
Alignment in C
Alignment in C(Haase; 2014)https://wr.informatik.uni-hamburg.de/_media/teaching/wintersemester_2013_2014/epc-14-haase-svenhendrik-alignmentinc-paper.pdf CのAlignmentについての簡潔な説明である。
日本語の非常に詳細で有名な解説ページは下のものがある。 データ型のアラインメントとは何か，なぜ必要なのか？
ワードとはそのコンピュータが最も自然に扱えるビットサイズである、と定義されている。 この定義に従うと、メモリから一度に読み出せるビット幅、と多くの場合には一致することが期待できるだろう。 現在主流の環境である64-bitコンピュータではワードサイズは8byte(64bit)ということになる。
特殊なCPU命令を発行すると256bit幅を一度に処理することなどもあり、またもちろんchar型などのより小さなサイズのデータを扱うこともある。 Alignment制約とはこれらのワードサイズと異なるデータがメモリ上に配置される際に、効率的に処理されるようにデータを配置するようにCPUが要求する制約である。
例えば8byteのint型データがメモリ上で2つのワードにまたがって配置されていたとする。 このとき、メモリから一度に8byteの読み出しが可能であるにも関わらず、実際のデータの読み出しは2ワードの読み出しが必要になってしまう。
word a b c d e f g h memory ... | _ _ _ _ _ a b c | d e f g h _ _ _ | ...
一部の環境ではこのようなメモリアクセス(Alignment違反)に対して、実際に2ワードを読みだすこともあり、また他の環境ではエラーにさえなることもある。 具体的にはRISCアーキテクチャ、ARMやMIPSではalignment違反はエラーを送出するようだ。 特殊用途のSSE命令などでも、適切にalignされていないデータに対しての計算結果は定義されないことが多い。 現代的なアーキテクチャでは、misalignedなアドレスへのアクセスが可能になっているものもあり、多くの場合には2アクセスによって成されるため、性能の劣化がある。 (最近の?)x86_64ではこの性能的なペナルティ無しでmisalignedなアドレスへのアクセスが可能だそうだ。
また、stack領域のalignmentは環境により様々であり、例えばLinuxでは昔は4bytes, 最近は16bytes, Windowsでは4bytes, OSXでは16bytesだそう。クロスアーキテクチャで動作する必要のあるようなプログラムを書く際には注意が必要である。(具体的には、attribute*1や-mstackrealignなどを使いrealignmentを行うことで対処するそうである。)
note: * clangの-Wpaddedオプションを付けるとpaddingが入った時にwarningを出してくれるので、手動でメモリ使用量の最適化をかけるときに利用することができる * 構造体のpaddingを押しつぶすattribute*2, #pragma pack, -fpack-structなどの方法があるが、これはABIの互換性を壊すことに注意する必要がある * コンパイラが最適化の中でSSEの命令を発行するときには、適切にalignmentを保ってくれる(例えば16byte alignmentになるように適切にpaddingを入れる)はずであり、そのためプログラマが明示的に指示せずとも16bytes alignmentなどにデータが配置されていることがあるかもしれない
