論文の概要: Dsat: A Native SAT Solver for Discrete Logic

• arxiv url: http://arxiv.org/abs/2605.09347v1
• Date: Sun, 10 May 2026 05:57:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:50.204211
• Title: Dsat: A Native SAT Solver for Discrete Logic
• Title（参考訳）: Dsat: 離散論理のためのネイティブSATソルバー
• Authors: Yaofang Zhang, Ken Zhou, Adnan Darwiche,
• Abstract要約: 我々は、変数が任意の値を取ることのできるブール論理の直接拡張である離散論理用のネイティブSATソルバを開発した。 CNFに対して適用されたCSPソルバと、二項化CNFに対して適用されたBoolean SATソルバと、ハイブリッドソルバとを経験的に比較することにより、開発したSATソルバの利点を解説する。
• 参考スコア（独自算出の注目度）: 7.054093620465401
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.
• Abstract（参考訳）: 離散変数は確率論的推論、計画、説明可能なAIなど、多くのアプリケーションで一般的である。 これらの応用にシンボリック推論技術が適用されると、離散変数を扱うための標準的な手法は、それらをブール変数にバイナライズしてSATソルバのようなブール計算機械の使用を可能にすることである。 しかし、この手法は計算と意味の両方の課題に直面することがある。 本研究では、変数が任意の値を取ることのできるブール論理の直接拡張である離散論理用のネイティブSATソルバを開発する。 提案する解法はBoolean SATソルバとよく似た設計であり, 単位分解能や節学習などの要素を持つが, 独立変数上でネイティブに動作する。 CNFに対して適用されたCSPソルバと、二項化CNFに対して適用されたBoolean SATソルバと、ハイブリッドソルバとを経験的に比較することにより、開発したSATソルバの利点を解説する。

関連論文リスト

• LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving [0.0]
  LangSATは自然言語入力と命題論理のギャップを埋める。 Lang2Logic は英語の文を Conjunctive Normal Form (CNF) に翻訳する。 SmartSATは、構造化グラフ表現として節変数の関係をエンコードする。
  論文  参考訳（メタデータ） (2025-12-04T01:47:06Z)
• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• Language Models can be Logical Solvers [99.40649402395725]
  論理解法の推論過程を直接エミュレートする新しい言語モデルであるLoGiPTを導入する。 LoGiPTは、導出的ソルバの見えない推論過程を明らかにして精錬することから導かれる、新しく構築された命令チューニングデータセットに基づいて微調整される。
  論文  参考訳（メタデータ） (2023-11-10T16:23:50Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
  本稿では、繰り返しニューラルネットワークを統合したGNNベースのアーキテクチャであるAsymSATを提案し、可変代入に対する依存予測を生成する。 実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
  論文  参考訳（メタデータ） (2023-04-18T05:33:33Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。 DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
  論文  参考訳（メタデータ） (2022-05-27T03:20:42Z)
• 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)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。