インメモリ計算でハイブリッドXOR–CNFブール充足可能性問題をネイティブに高速化する

なぜ問題解決の高速化が重要か

オンライン通信の保護から高速な電子機器の設計に至るまで、私たちの日常を形作る多くの課題は、コンピュータに「この大きな論理規則を真にするスイッチの組み合わせは存在するか？」というはい・いいえの問いを投げかけることに帰着します。これがブール充足可能性（SAT）問題です。SATは広く難しい問題として知られており、課題の規模と重要性が増すにつれて、それを解くために必要な時間とエネルギーが大きなボトルネックになっています。本論文は、数学的表現とハードウェアの両方を再設計してメモリ内で協調的に動作させることで、SAT解法を加速する新しい方法を探ります。

複雑な規則をより単純な構成要素に変える

従来のSATソルバーは多くの場合、OR（論理和）条件から構成される一つの様式で問題を記述します。しかし、無線信号の復号、チップの故障検査、ある種の暗号解読など、多くの実際の産業問題は自然にORと排他的論理和（XOR、入力が1つ変わるとパリティが反転する種類のチェック）を混在させます。現在のツールはしばしばこれらのXORルールをORのみで書き換えることを強いるため、問題のサイズが膨らみ、処理が遅くなります。著者らは代わりに両方の種類の規則を維持し、問題が現実に生じる形により近いハイブリッドな記述を採用します。

より少ない要素でより多くを達成する

研究者たちは、暗号学由来のベンチマーク群や古典的な最小不一致パリティ問題など、いくつかのベンチマークファミリでこのハイブリッド記述を従来手法と比較しました。隠れたXOR構造を自動的に再構成し、まず賢い簡略化を適用することで、混合表現は変数数を数倍にまで削減し、規則（節）の数を概ね4～5倍程度削減できることを示しています。言い換えれば、XORとORを共存させることで、同じ論理的問いをはるかに少ない構成要素で表現できることが多いのです。問題が小さくなるとソフトウェアだけでなく、同時に一度に格納できる規則数が厳しく制限される専用ハードウェアにも有利になります。

メモリチップに計算させる

この効率的な記述を活用するため、チームは専用の「インメモリ計算」アクセラレータを設計しました。プロセッサとメモリ間でデータを何度も往復させる代わりに、この装置はメムリスタと呼ばれる微小な電子素子のグリッド内、つまりデータが格納される場所で多くの計算を実行します。既知の局所探索戦略であるWalkSATを、XOR–ORの混合規則をネイティブに扱える新しい変種WalkSAT-XNFへ適応させました。アルゴリズムの各ステップ—破られている節の評価、各変数の重要度推定、行き詰まりを抜けるためのノイズ付加、最適候補の反転—はクロスバー配列上のアナログ回路で直接実装され、どの変数を次に反転させるかを選ぶための簡易な支援回路が伴います。

実験室とシミュレーションで動作を実証

著者らはまずメムリスタチップを用いた小さなプロトタイプを構築し、製造ばらつきや電気的ノイズがある状況でもアナログハードウェアが節を忠実に評価し探索を導けることを示しました。控えめなサイズのテストインスタンスでの実験は、ハードウェアの挙動が理想的なシミュレーションとよく一致することを示しています。さらに28ナノメートル設計をモデル化し、暗号問題やパリティ問題のファミリでベンチマークを行いました。ハイブリッド記述はより少ない節に多くの情報を詰め込めるため、アクセラレータはオンチップメモリをはるかに少なく済ませ、1ステップ当たりの消費エネルギーもORのみのバージョンより大幅に低くなります。総合的に見て、ハイブリッドなインメモリソルバは、従来のCPU上で動く最先端のソフトウェアSATソルバと比べて約10倍の高速化と約1000倍のエネルギー効率改善を達成しました。

将来のコンピュータにとっての意義

平たく言えば、本研究は、論理規則の書き方をメモリベースの新しいハードウェアの計算様式に合わせることで、特定の難問をはるかに速くかつ低消費電力で解けることを示しています。チップ内でXORとORの両方をネイティブにサポートすることで、提案されたアクセラレータは暗号、通信、回路設計といった現実的な課題を、より小型で冷却負担が少なく迅速なハードウェアで扱えます。計算システムがエネルギーと速度の限界にますます直面する中、この種の問題特化型インメモリ方式は重要なデジタルインフラの安全性と効率を保つ助けになる可能性があります。

引用: Im, H., Böhm, F., Pedretti, G. et al. Accelerating hybrid XOR–CNF Boolean satisfiability problems natively with in-memory computing. Nat Commun 17, 2922 (2026). https://doi.org/10.1038/s41467-026-69465-2

キーワード: ブール充足可能性, インメモリ計算, メムリスタ・クロスバー, ハードウェアアクセラレータ, 暗号学