Parallel Execution of Constraint Handling Rules on a Graphical Processing Unit
という論文を読みました。
リンク
リンク切れている場合は論文名で検索してください。

Constraint Handling Rulesの開発者のThom Fr¨uhwirth さん達が書いた論文で、CHRをGPU上で実行させる方法がCUDAのコード込みで書いてあります。

Constraint Handling Rulesに関して自分がわかっているレベル(≒あまりわかっていない)で簡単に説明すると、CHRは基本的には記述された一連の制約を論理的に同等かつよりシンプルなものにしたり、何かに変換（自作の制約で書いた記述 → 組み込み述語のみ使用した記述に変換など）したりします。

例えばECLiPSeではPropiaとは別にCHRを使用しても自作の制約が定義出来ます。

まず以下の3種類のいずれかの構文でルールを記述しておきます。(これが自作制約となります)
CHRには以下の3つしかルールがありません。
・simplification
　　Head1,Head2 <=> Guard | Body
・propagation
　　Head1,Head2 => Guard | Body
・simpagation
　　Head1¥Head2 <=> Guard | Body
（HeadもGuardもBodyも普通のPrologのCallable Termで書きます。
GuardとBodyの部分は複数の述語を書いて良い。Headの部分は最大2つの述語のみ（ECLiPSeの場合。3つ以上が不可なのは以下に述べる述語のピックアップの際の効率の問題らしいです）→すみません訂正します。CHRの昔のライブラリでは2つのみでしたが、新しいECHライブラリでは3つ以上可能でした）

動作の仕組みなのですが、上記で定義した制約を含む述語群を連言（=AND。カンマ区切りの普通のPrologの表現）で記述すると、CHRの機構はそれらの述語群の中から2つピックアップし、
・上記のHead1,Head2にパターンマッチ
・GuardがTrueとなる
を満たすものを見つけると、以下のルールに従ってピックアップした2つの述語を「書き替えて」しまいます（これをfire[発火]と呼ぶ）そしてその際にBodyの実行可能な述語は実行してしまいます。
また、Guardの部分は常時チェックされる番犬のような動作をしていて、例えばguardにnonvar(A)みたいな記述をしていた際、別の処理でAに何か値を設定した場合、その瞬間にGuardのチェックが通り対応するBodyが発火されます（ECLiPSeのsuspend機構を使って実装されている）
simplificationの場合はBodyに書き換え
propagationの場合はHead1,Head2そのままでBodyの述語を追加
simpagationはHead2のみBodyに書き換え(Head1は残す)

上記の変換を適用できるルールがなくなるまで繰り返す（2つ述語ピックアップ→Head1,Head2にマッチングするかチェック→GuardがTrueかチェック→ルールに従いHead1,Head2を書き換え）
どうも書き換え中のルール群をconstraint storeと呼んでいるようです。

ちなみに上記一連の処理中にはバックトラックは発生しません。
CHRの動作を「コミッテドチョイス」と言うらしいのですが、CHRの機構がどの述語をピックアップするか勝手に決めるのでプログラマはコントロールできない（選択を委託する）という意味かもしれません。
また、Headの部分は２つじゃなくて1つでも良いです。

CHRは基本的には上記の書き換えを行うのみなので、用途は特に制約の表現のみにとどまらず、サンプルを見ると
　最大公約数の計算
　ガウスの消去法
　高速フーリエ変換
　マージソート
など、色々な応用があります。

めちゃめちゃ端折ってますが上記がCHRの基本動作です。

記述した制約群をどのような組み合わせでピックアップ・変換したとしても必ず最終的に生成される述語群が同じになるようなとき、Confluence（合流）性を持つと言うそうです。

Confluence性はどのようにすれば担保されるかなのですが、以下の論文に書いてありますが自分はまだ理解できていない（論理学の用語がたくさん使用されてて難しいため）どうも冗長なルールを追加することにより合流性が担保されるようです。

Theory and practice of constraint handling rules
リンク切れしている場合は論文名で検索してください。

Confluence性を満たす場合CHRが並列処理に非常に向いているとのことで、理屈では確かにそうだなと自分も納得しました。

前置きが長くなりましたが、上記を踏まえたうえでGPUでCHRを使った上記の論文を読んだわけです（GPUは数千コア積んでいるものもあり単純な計算を同時に行うのに非常に有力）
論文の内容はCUDAコードが実際に記載されていて実装イメージがしやすいものでした。
しかし、ルールの述語自体をCUDAコンパイル用のコードで書いているため、あまり汎用性がないのではないという気がしました。
使う側は当然任意の述語を使いたいのですが、論文のやり方ではそのたびに新たなプログラムをCUDA用に書いてコンパイルしなくてはならないのでは？と感じました。
あまりGPUのことわかってないですが、if文を多用するプログラムは遅くなるなど、性能を100%出すためにいろいろ条件があるようです。
現状ではCHRをGPUの速度を100%出し切って実行するのは難しいのかな、と感じました。
ただ理論的にCHRのいろいろな性質が証明されているので、ハードウェア側でCHRに向いた実装が実現されたら、かなり望みがあるような気がします。

余談ですが「CHRには3つしかルールがない」と書きましたが、
・simpagation
　　Head1¥Head2 <=> Guard | Body
の、
・simplification はこれの Head1 がないバージョン（Head2がBodyに書き換えられる)
・propagation はこれの Head2 がないバージョン(Head1そのままでBodyが追加される)
となるので実質はsimpagationだけで良いみたいな文章をどこかで読みました。