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ソルバの有用性を実証する。

関連論文リスト

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)
Faith and Fate: Limits of Transformers on Compositionality [109.79516190693415]
3つの代表的構成課題にまたがる変圧器大言語モデルの限界について検討する。これらのタスクは、問題をサブステップに分割し、これらのステップを正確な答えに合成する必要があります。実験結果から,多段階合成推論を線形化部分グラフマッチングに還元することにより,トランスフォーマーLLMが構成課題を解くことが示唆された。
論文参考訳（メタデータ） (2023-05-29T23:24:14Z)
Large Language Model Guided Tree-of-Thought [0.0]
自動回帰型大規模言語モデル(LLM)の問題解決能力向上を目的とした新しいアプローチであるTree-of-Thought(ToT)フレームワークを導入する。 ToTテクニックは、試行錯誤によって複雑な推論タスクを解決するための人間の心のアプローチにインスパイアされている。実験結果から,ToTフレームワークはスドクパズル解法の成功率を大幅に向上させることができることがわかった。
論文参考訳（メタデータ） (2023-05-15T01:18:23Z)
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)
An efficient constraint based framework forhandling floating point SMT problems [0.5161531917413706]
本稿では,浮動小数点検証問題に対する新しい制約プログラミングフレームワークである,私たちによる2019年版を紹介する。私たちにとって、フロートに対する制約は第一級のオブジェクトであり、浮動小数点領域の構造を公開して活用することを目的としています。
論文参考訳（メタデータ） (2020-02-27T21:11:22Z)

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