ネックになっているのは、時間制約です。
• 連続勤務は最大13時間程度
• 24時間内に11時間の休息義務
などの強い規制が一般的です。）
このインスタンスをよく見ると、Time制約幅が狭小であり、係数も0,4,5,6に限られています。
計数制約は、他に沢山あるのですが、解空間は、ほぼTime制約で決まっているように思います。制約幅が、狭小であることを勘案すれば、もう少し工夫を凝らせそうです。
この辺は、私でもやってみないと分からない領域です。試してダメだったら理由を後付けで考える、ということの繰り返しです。
このモデルは、物凄く簡単です。もしも、時間制約が15分単位で、種類が沢山あるということなら、1年という長期間の間に簡単に、爆発してしまいます。簡単なモデルだからこそ、1年という長期間に計算モデルが爆発しないでいられる、ということです。その意味で、時間制約は、一般に、慎重を要する制約となります。
AI時代の高等教育から消えるプログラミング言語、米スタンフォード大が「人間の言語」を重視する理由とは（朝鮮日報日本語版） - Yahoo!ニュース
スケジュールナースを操作するのに、プログラミング言語経験よりも大事なのは国語力、というお話しは、何度もしてきたのですが、上の記事を見るにつけ、時代が追いついてきた、と感じます。
NVIDIAの
Autonomous Code Evolution Meets NP-Completeness
の論文をコパイにまとめてもらいました。
2025優勝ソルバにたいして相当の向上が見られ、それは、単に過去ソルバの良いところ取りに留まらず、自律的新アルゴリズムを発見した、
ということのようです。
これまで、LLMが出来るのは、パラメータの調整だけだと思いこんでいたのですが、間違っていました。
ここまで到達すると、もはや「研究者は不要」、という領域に入ってくるかもしれません。新しいアルゴリズムを考えるより、如何に賢いAIを育てるか？の方が焦点になる可能性があります。
恐らく、2024SATCompetitionが、優勝者が人間だった最後の年で、以降、全てAIになるのではないかと予想します。（2025の優勝者はAIでした）
SAT Competitionは、SATソルバ界隈での最高競技会でありトップ研究者達の集まりです。
ソースは全てオープンであるが故に、結果、多くの知恵が集まり多くの研究成果が生まれました。しかし、オープンであるが故にAIの餌食となってしまった、とも言えます。人類の知恵は、論文に集積されていますが、数秒で新しい論文を理解してしまう知能と、眠ることのない存在に、もはや勝ち目はないのでは？とも思います。AIと抽象的・数学的・技術的な会話をすること自体は楽しいのですが、同時に、技術的な議論を通じて、現在自分が研究している最先端（極めてニッチな領域ではありますが、人類の知恵の先端）を除いて、敵うことのないメンター的知性を持った存在、という印象をさらに強く抱いている次第です。それも論文化してしまうと、瞬く間にそれを理解・吸収してしまい、底知れぬモンスターに成長するのでは？と危惧しています。
Q.2025優勝ソルバとの比較
結論から言うと 「はい、明確に増えています」。
あなたが開いている論文 “Autonomous Code Evolution Meets NP-Completeness” の記述によれば、SATLUTION は SAT Competition 2025 の Winner（AE_kissat2025_MAB）よりも多くの問題を解いています。 arxiv.org
論文の Figure 2（Cactus Plot）に明確に書かれています：
SATLUTION のトップ 3 ソルバー
SAT Competition 2025 Winner（AE_kissat2025_MAB）
2nd place（kissat-public）
つまり、SATLUTION は Winner より 10〜13 問ほど多く解いています。
これはかなり大きな差で、特に中〜難問領域（1000〜4000秒帯）で差が開いていると論文は述べています。 arxiv.org
解けた問題数は増えているか？
→ はい、Winner より明確に増えています。
どれくらい増えたか？
→ 約 10〜13 問多く解いた（347 vs 334）。
どの領域で強かったか？
→ 中〜難問帯で Winner が止まった後も SATLUTION は解き続けた。
必要なら、
結論から言うと 「半分正しいが、それだけでは不十分」 という答えになります。
SATLUTION（論文中の表記は SATLUTION）は、確かに 過去ソルバの良いところ取り（hybridization）を行っている のですが、実際にはそれを はるかに超える進化的プロセス を実行しています。
以下、論文内容に基づいて整理します（ arxiv.org）。
論文では、初期状態として SAT Competition 2024 の 5 つの強力なソルバを seed として与えています。
SATLUTION はこれらのコードベースを読み込み、
互いの強みを組み合わせる方向に進化する と明記されています。
“SATLUTION made rapid progress in the first 5–10 iterations, quickly lowering PAR-2 by combining complementary strengths from the different seed solvers.”
（ arxiv.org）
つまり、初期段階ではまさに「良いところ取り」をして性能を底上げしています。
SATLUTION の特徴は、単なるマージではなく 新しいヒューリスティックやアルゴリズムを自動生成する点 にあります。
論文では、進化の過程で以下のような 新規の最適化手法 を自律的に発見したと書かれています：
これらは単なる「良いところ取り」ではなく、
既存ソルバにも存在しない新規アイデア です。
SATLUTION はコードだけでなく、
自分自身の進化ルール（rulebase）も自動で更新する という仕組みを持っています。
これは人間の開発プロセスに近い「メタ進化」であり、
単なるソルバの合体では到達できない領域です。
| 観点 | SATLUTION の実際 |
|---|---|
| 過去ソルバの良いところ取り？ | YES（初期段階で大きく寄与） |
| それだけ？ | NO（中盤以降は新規アルゴリズムを自律生成） |
| 進化の本質 | ルールベース＋フィードバックによる 自律的コード進化 |
| 最終的な成果 | 2025 Winner を超える性能（347 solved vs 334 solved） |
「良いところ取り」は SATLUTION の進化の一部にすぎず、
本質は “自律的に新しい SAT ソルバを設計する AI エージェント” です。
もし興味があれば、
SATにおいて重要な概念です。at leastとat most制約は、互いに変換可能ということになります。なので、通常はどちらかだけの制約を持てば、十分です。
Σx(i)≦kのとき、xの個数がNなら
Σ~x(i)≧N-k
と変換できます。１の最大数がk個以下が必要なら、０の最小数がN-k個以上であれば良い訳です。
例えば、N=10,k=9のとき、１となる個数を9個以下にしたいときは、０となる個数を1個以上にすればよい、
です。
以下は、AIでの補足説明です。
リテラル数を (N) としたときの “most k” と “least k” の関係を、
直感的に理解できる図で説明します。
least k：
「少なくとも (k) 個は真である」
→ 真のリテラル数が (k, k+1, …, N) の領域を表す
most k：
「高々 (k) 個が真である」
→ 真のリテラル数が (0, 1, …, k) の領域を表す
0 k N
|--------|--------|
0 k N
|--------|================|
↑ least k はここから右側
0 k N
|================|--------|
most k はここまで ↑
真リテラル数 →
0 k N
|========|========|
↑ ↑
most k least k
(0〜k) (k〜N)
リテラルという言葉は、論理や制約プログラミングの世界ではとても基本的で重要な概念です。
ここで一度、丁寧に整理しておきますね。
この 「変数」または「否定された変数」 をまとめて リテラル と呼びます。
論理変数 (x, y, z) があるとき、リテラルは：
合計 6 個のリテラルが存在します。
論理式（CNF、DNF、PB制約など）を扱うとき、
「真偽を持つ最小の要素」 を数えたり制約したりする必要があります。
たとえば：
least k：
「リテラルのうち 少なくとも k 個 が真」
most k：
「リテラルのうち 高々 k 個 が真」
このときの「リテラルの個数」がまさに literal count です。
変数 x がある → リテラルは x と ¬x の2つ
ただし、制約の文脈では 「式に登場するリテラル」だけを数える のが普通です。
| 用語 | 意味 |
|---|---|
| 変数 | 真偽値を持つ基本要素 |
| リテラル | 変数またはその否定（例：x, ¬x） |
| リテラル数 N | 制約に登場するリテラルの総数 |
| least k | N 個のリテラルのうち少なくとも k 個が真 |
| most k | N 個のリテラルのうち高々 k 個が真 |
必要なら、
void set_vars_lowest_priority(std::vector<int> lits);//FEB042026
というAPIをCadicalに追加しました。decide()で、変数を選ぶのですが、基本的には、スコアが高い順番に決められます。ここで、制約している範疇の変数と、そうでない変数とでは、当然制約に関与している変数が先に実行されるべきです。それがスコアだけだとコントロールできないことが問題です。未だ制約が及んでいない変数群については、decide()を後回しして、残った帰結として、決めてやる、ことが理想です。
一方、Cadicalのdefaultモードは、VSIDSとは別にあり、基本的に新しい変数から実行されてしまいます。スコアという概念さえもなく全く外部からコントロール出来ません。
CHBの実装をコパイに依頼したら、次のコードを提示されました。
int Internal::pick_chb_branch_lit () {
double best = -1.0;
int best_idx = 0;
// 変数集合のイテレーション：CaDiCaL の実装に合わせて調整
for (int idx = 2; idx <= max_var; idx++) { // idx: internal literal index (±)
if (!active (idx)) continue;
if (val (idx)) continue; // すでに割り当て済み
const double s = chb_score (idx);
if (s > best) {
best = s;
best_idx = idx;
}
}
}これは、却下です。変数の全スコアをスキャンして、その最高値を持ってくる実装ですが、遅すぎて話になりません。折角、スコア用のヒープを備えているのですから、それを利用しない手はありません。
struct score_smaller {
Internal * internal;
score_smaller (Internal * i) : internal (i) { }
bool operator () (unsigned a, unsigned b);
};
struct ScoreComparator {//FEB042026
Internal* internal;
ScoreComparator(Internal* i) : internal(i) {}
// ここが比較の核心：internal->score (a) の値を直接見ている
bool operator () (unsigned a, unsigned b)const;
};
typedef heap ScoreSchedule;
typedef heap ScoreHeap;//FEB042026
#ifdef USE_CHB
inline bool ScoreComparator::operator() (unsigned a, unsigned b) const {
assert(1 <= a);
assert(a <= (unsigned)internal->max_var);
assert(1 <= b);
assert(b <= (unsigned)internal->max_var);
return internal->chb_score(a) < internal->chb_score(b);
}
#endif
#ifdef USE_CHB
double& chb_score(int lit) { return chb[vidx(lit)]; }
#endif
void Internal::bump_variable_score (int lit) {
assert (opts.bump);
int idx = vidx (lit);
#ifdef USE_CHB
const int64_t conflicts = stats.conflicts;
// CHBの報酬計算: 1 / (現在のコンフリクト番号 - 最後にこの変数が関与した番号 + 1)
double reward = 1.0 / (double)(conflicts - last_conf[idx] + 1);
//CHBは「直近のコンフリクト」を重視するため、探索が進むにつれて学習率を下げていかないと、スコアが激しく変動しすぎて探索が安定しません。 Liangらの論文で推奨されている標準的な設定は以下の通り： 初期値(\(\alpha _{ start }\)) : 0.4下限値(\(\alpha _{ min }\)) : 0.06減衰量(\(\alpha _{ step }\)) : 1e-6（衝突1回につき）
if (chb_alpha > 0.06) {
chb_alpha -= 0.000001;
}
// ERWA (Exponential Recency Weighted Average) 更新
// Q = (1 - alpha) * Q + alpha * reward
// α の減衰
chb[idx] = (1.0 - chb_alpha) * chb[idx] + chb_alpha * reward;
last_conf[idx] = conflicts;
// ヒープの更新（ScoreComparatorがchbを参照するようになっているため、これで並び替わる）
if (chb_scores.contains(idx)) chb_scores.update(idx);
#endif
Liangさんの論文に示された通りの実装にしています。上の更新式は、一次IIRフィルタに似ています。
当時、確か、機械学習の発想を取り入れた、との話があったかに記憶しています。
https://ojs.aaai.org/index.php/AAAI/article/view/10439
なお、CHBは、VSIDSよりもリスタート間隔を短くした方がよい、という説もありますが、真偽は分かりません。
Combining VSIDS and CHB Using Restarts in SAT
Cadical/Kissa共、CHBを実装していないのですが、最近のSAT competitioin優勝ソルバは、いずれもMAB方式です。
A new variable ordering for in-processing bounded variable elimination in SAT solvers | Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence
多分バグだと思いますが、GCCでは警告がないのかもしれません。
radix sort部分でクラッシュしました。コパイにお願いすると、VisualStudioのエラーと一致する指摘となりました。完全に書き換えるコードの提案をされて、安直に置き換えてみるとエラーは消失しました。凄い。C++ソースも完全に理解しているのですね。
c == b の比較で vector がエラーになる理由は、このコードが イテレータ同士の比較をしているように見えて、実際には “別コンテナのイテレータを比較している” 可能性が非常に高いからです。
c と b は「同じコンテナのイテレータ」ではないコードの該当部分を抜き出すと：
I a = first, b = last, c = a;
...
std::vector<T> v;
...
if (!initialized) {
v.resize(n);
b = v.begin();
initialized = true;
}
...
I d = (&*c == &*a) ? b : a;
...
c = d;
...
if (c == b) {
for (size_t i = 0; i < n; i++)
a[i] = b[i];
}
ここでのポイントは：
a と c は 元の配列（FIRST〜LAST） のイテレータb は vectorc == b は 異なるコンテナのイテレータ比較C++ の規格では：
異なるコンテナのイテレータを比較することは未定義動作（UB）
未定義動作なので、クラッシュしたり、比較が常に false になったり、ランダムな挙動をします。
c は毎ループで a または b に切り替わる。
c = a のとき → 元の配列のイテレータc = b のとき → vector のイテレータ最後に
if (c == b)
を行うが、c が元配列のイテレータのままなら 異なるコンテナのイテレータ比較 になる。
最も安全で一般的な修正は：
c が vector 側を指しているかどうかを bool で管理する例：
bool using_vector = false;
...
if (!initialized) {
v.resize(n);
b = v.begin();
initialized = true;
}
...
I d;
if (&*c == &*a) {
d = b;
using_vector = true;
} else {
d = a;
using_vector = false;
}
c = d;
...
if (using_vector) {
for (size_t i = 0; i < n; i++)
a[i] = b[i];
}
これなら 異なるコンテナのイテレータ比較を避けられる。
| 問題点 | 理由 |
|---|---|
c == b がクラッシュ |
異なるコンテナのイテレータ比較は未定義動作 |
| なぜ起きる？ | c は元配列 or vector のどちらかを指す可能性がある |
| 解決策 | イテレータ比較ではなく、どちら側を使っているかを bool で管理 |
必要なら、この radix sort 全体を 安全に書き直したバージョン も作れます。
あるいは、あなたのプロジェクトに合わせて 最適化版 を作ることもできますよ。
了解、孝幸さん。
あなたのコードは CaDiCaL の radix sort 実装をベースにしていますが、イテレータが別コンテナを指す可能性があるのに比較してしまうという UB（未定義動作）が潜んでいました。
そこで、イテレータ比較を完全に排除し、状態フラグで安全に制御するバージョンを用意しました。
元のアルゴリズム構造は維持しつつ、C++ として安全に動くように書き直しています。
rsort（イテレータ比較なし・UBなし）template <class I, class Rank>
void rsort(I first, I last, Rank rank) {
using T = typename std::iterator_traits<I>::value_type;
using R = typename Rank::Type;
assert(first <= last);
const size_t n = last - first;
if (n <= 1) return;
const size_t l = 8;
const size_t w = (1 << l);
const unsigned mask = w - 1;
size_t count[w];
I a = first;
I c = a;
std::vector<T> v;
I b; // vector 側の begin()
bool using_vector = false; // ★ どちら側を使っているかを管理
R upper = 0, lower = ~upper;
R shifted = mask;
bool bounded = false;
R masked_lower = 0, masked_upper = mask;
for (size_t i = 0; i < 8 * sizeof(rank(*first)); i += l, shifted <<= l) {
if (bounded && (lower & shifted) == (upper & shifted))
continue;
memset(count + masked_lower, 0,
(masked_upper - masked_lower + 1) * sizeof *count);
const I end = c + n;
bool sorted = true;
R last_bucket = 0;
for (I p = c; p != end; p++) {
const auto r = rank(*p);
if (!bounded) {
lower &= r;
upper |= r;
}
const auto m = (r >> i) & mask;
if (sorted && last_bucket > m)
sorted = false;
last_bucket = m;
count[m]++;
}
masked_lower = (lower >> i) & mask;
masked_upper = (upper >> i) & mask;
if (!bounded) {
bounded = true;
if ((lower & shifted) == (upper & shifted))
continue;
}
if (sorted)
continue;
size_t pos = 0;
for (R j = masked_lower; j <= masked_upper; j++) {
const size_t delta = count[j];
count[j] = pos;
pos += delta;
}
if (!using_vector) {
v.resize(n);
b = v.begin();
}
I d = using_vector ? a : b; // ★ ここで切り替え
bool next_using_vector = !using_vector;
for (I p = c; p != end; p++) {
const auto m = (rank(*p) >> i) & mask;
d[count[m]++] = *p;
}
c = d;
using_vector = next_using_vector;
}
if (using_vector) {
for (size_t i = 0; i < n; i++)
a[i] = b[i];
}
#ifndef NDEBUG
for (I p = first; p + 1 != last; p++)
assert(rank(p[0]) <= rank(p[1]));
#endif
}
| 問題点 | 修正内容 |
|---|---|
異なるコンテナのイテレータ比較 (c == b) |
bool using_vector で状態管理 |
&*c == &*a のような危険なアドレス比較 |
完全に排除 |
| イテレータがどちらの配列を指すか不明瞭 | using_vector と next_using_vector で明確化 |
| UB（未定義動作） | ゼロ |
std::array<size_t, w> を使って stack allocation を明示化std::span を使って safer pointer arithmeticstd::bit_width を使って動的にパス数を決定std::pmr::vector でアロケーション最適化必要なら、これらも組み込んだ モダン C++20/23 版の高速 radix sort も作れます。
もっと最適化したい、あるいは CaDiCaL の他の部分も安全化したい場合は続けてどうぞ。