2026年2月5日木曜日

Cadical CHBを外部からコントロールするAPIを追加

   void set_vars_lowest_priority(std::vector<int> lits);//FEB042026

というAPIをCadicalに追加しました。decide()で、変数を選ぶのですが、基本的には、スコアが高い順番に決められます。ここで、制約している範疇の変数と、そうでない変数とでは、当然制約に関与している変数が先に実行されるべきです。それがスコアだけだとコントロールできないことが問題です。未だ制約が及んでいない変数群については、decide()を後回しして、残った帰結として、決めてやる、ことが理想です。

一方、Cadicalのdefaultモードは、VSIDSとは別にあり、基本的に新しい変数から実行されてしまいます。スコアという概念さえもなく全く外部からコントロール出来ません。

その解決策として、CHBを導入、さらにAPIによるコントロールにより、制約に関係した変数をFirst、関係していない変数を最後に持ってくることを行えるようにします。これは、現在のスケジュールナースが行っている処理であって新しいものではありません。しかしながら、今回、Cadical上では、そのようなAPIは、存在していないので、自前で改造する必要がありました。




0 件のコメント:

コメントを投稿