Fugu-MT 論文翻訳(概要): Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles

論文の概要: Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles

arxiv url: http://arxiv.org/abs/2501.08569v1
Date: Wed, 15 Jan 2025 04:31:56 GMT
ステータス: 翻訳完了
システム内更新日: 2025-01-16 15:51:55.680483
Title: Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
Title（参考訳）: 大規模スドクノズルにおけるSATおよびSMT解法の評価
Authors: Liam Davis, Tairan Ji,
Abstract要約: Z3, CVC5, DPLL(T) における現代の SMT ソルバの性能を DPLL の SAT ソルバに対して評価した。以上の結果から,現代のSMTソルバは従来のSATソルバよりも有意に優れていた。
参考スコア（独自算出の注目度）: 0.0
License:
Abstract: Modern SMT solvers have revolutionized the approach to constraint satisfaction problems by integrating advanced theory reasoning and encoding techniques. In this work, we evaluate the performance of modern SMT solvers in Z3, CVC5 and DPLL(T) against a standard SAT solver in DPLL. By benchmarking these solvers on novel, diverse 25x25 Sudoku puzzles of various difficulty levels created by our improved Sudoku generator, we examine the impact of advanced theory reasoning and encoding techniques. Our findings demonstrate that modern SMT solvers significantly outperform classical SAT solvers. This work highlights the evolution of logical solvers and exemplifies the utility of SMT solvers in addressing large-scale constraint satisfaction problems.
Abstract（参考訳）: 現代のSMTソルバは、高度な理論推論と符号化技術を統合することにより、満足度問題に対するアプローチに革命をもたらした。本研究では,Z3, CVC5, DPLL(T) における最新の SMT ソルバの性能を DPLL の標準SAT ソルバに対して評価する。改良したSudokuジェネレータの難易度を25×25の多種多様なSudokuパズルにベンチマークすることにより,高度な理論推論と符号化技術の影響を検証した。以上の結果から,現代のSMTソルバは従来のSATソルバよりも有意に優れていた。この研究は、論理解法の進化を強調し、大規模制約満足度問題に対処する上でのSMTソルバの有用性を実証する。

関連論文リスト

SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation [13.056487325961688]
Satisfiability(SAT)問題は、ソフトウェア工学における重要な応用において、中核的な課題である。本稿では,大規模言語モデル(LLM)を利用してSAT解決戦略の自動発見と最適化を行う新しいフレームワークであるSolSearchを提案する。
論文参考訳（メタデータ） (2025-02-20T07:25:21Z)
MATH-Perturb: Benchmarking LLMs' Math Reasoning Abilities against Hard Perturbations [90.07275414500154]
各種モデルにおけるMATH-P-Hardの性能低下を観察する。また、学習した問題解決スキルを盲目的に適用する新しい形態の記憶に関する懸念も提起する。
論文参考訳（メタデータ） (2025-02-10T13:31:46Z)
Smart Cubing for Graph Search: A Comparative Study [15.989407883187962]
立方体とコンカヤによる並列解法はSATソルバをハードインスタンスに拡張するための重要な方法である。キューブ・アンド・コンカーは純粋なSAT問題に対して成功したが、SATソルバへの応用はプロパゲータによって拡張され、ユニークな課題が提示される。本研究では, SATモジュロ対称性(SMS)を用いて, 対称性を破るプロパゲータが等方性グラフを除去する制約を学習することで探索空間を減少させる問題について検討する。
論文参考訳（メタデータ） (2025-01-27T22:15:54Z)
Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems [25.0042181817455]
本稿では,大言語モデルとオフ・ザ・シェルフ定理証明器を統合したマルチエージェントシステムZPSを紹介する。このシステムは、問題をより小さく管理可能な部分に分割することで、複雑なパズル解決作業に取り組む。また,問題解の正当性を評価するための自動グリッドパズルグレーダを導入し,ユーザスタディで評価することで,自動グレーダが信頼性が高いことを示す。
論文参考訳（メタデータ） (2024-07-04T14:22:25Z)
Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [7.348176676723853]
我々は、Z3 SMTソルバの一部として、Z3alphaと呼ばれる手法を実装した。 Z3alphaは、デフォルトのZ3ソルバであるSOTA合成ツールFastSMTや、ほとんどのベンチマークでCVC5ソルバよりも優れた性能を示している。
論文参考訳（メタデータ） (2024-01-30T16:47:30Z)
SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
大規模言語モデル(LLM)は人工知能の大幅な進歩を導いた。数学的問題を解く能力を高めるために,textbfSEquential subtextbfGoal textbfOptimization (SEGO) という新しいフレームワークを提案する。
論文参考訳（メタデータ） (2023-10-19T17:56:40Z)
The Machine Learning for Combinatorial Optimization Competition (ML4CO): Results and Insights [59.93939636422896]
ML4COは、キーコンポーネントを置き換えることで最先端の最適化問題を解決することを目的としている。このコンペティションでは、最高の実現可能なソリューションを見つけること、最も厳密な最適性証明書を生成すること、適切なルーティング設定を提供すること、という3つの課題があった。
論文参考訳（メタデータ） (2022-03-04T17:06:00Z)
Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文参考訳（メタデータ） (2022-03-02T05:14:12Z)
Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文参考訳（メタデータ） (2021-07-15T04:47:35Z)
Learning by Fixing: Solving Math Word Problems with Weak Supervision [70.62896781438694]
数学用語問題(mwps)の従来のニューラルネットワークソルバは、完全な監視によって学習され、多様なソリューションを生み出すことができない。 MWPを学習するためのテキスト弱教師付きパラダイムを提案する。この手法は最終回答のアノテーションのみを必要とし、単一の問題に対して様々な解決策を生成できる。
論文参考訳（メタデータ） (2020-12-19T03:10:21Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。