補助変数を用いたより迅速な認証された対称性破壊

対称性破壊は現代の組合せソルバーにおいて重要な技術ですが、その実装が正確であることを確信するのは難しいです。最も成功しているアプローチは、ソルバーが解を出力するだけでなく、正しさを証明する数学的証明も出力する認証ソルバーを用いることです。この証明は、定理の中で対称性の論理を正当化することを要求しますが、これを効率的に行う方法の開発は長年の課題でした。本研究では、補助変数を用いて順序を符号化する新しい手法を提案し、これにより理論的および実践的に速度向上が得られることを実証しています。実験は、最新のsatsuma対称性破壊器とVeriPB証明検証ツールチェーンを用いて行いました。