Sentient：制約ソルバーにおける無限大との格闘
2025-04-12
この記事では、制約ソルバーSentientにおける無限大の取り扱いに関する課題を深く掘り下げています。Sentientは、問題をブール方程式に変換することで制約充足問題を解決するプログラミング言語です。コンピュータにおける整数は有限ビット数で表現されるため、Sentientは数学的な意味での無限の整数を直接扱うことができません。著者は、整数のビット数を段階的に増やすことで無限空間を近似する、近似に基づく解決策を提案しています。この記事では、効率性を高め、冗長な探索を回避するために、増分SATソルバーIPASIRを活用する方法について議論しています。また、配列や最適化問題の処理など、より複雑なシナリオへのこのアプローチの拡張についても探求し、最終的にSentientが将来チューリング完全になる可能性にも触れています。