Daily Arxiv

世界中で発行される人工知能関連の論文をまとめるページです。
このページはGoogle Geminiを活用して要約し、非営利で運営しています。
論文の著作権は著者および関連機関にあり、共有する際は出典を明記してください。

Approximate SMT Counting Beyond Discrete Domains

Created by
  • Haebom

作者

Arijit Shaw, Kuldeep S. Meel

概要

本論文は、ハイブリッドSatisfiability Modulo Theory（式）のモデルカウント問題を解決するために、pactと呼ばれる新しいSMTモデルカウンタを提示します。既存のビットブラスティングベースのアプローチは離散変数に限定される限界を有するが、pactはハッシュベースの近似モデルカウントを利用して理論的保証の下で解の数を推定する。 pactは投影変数に対してログレベルのSMTソルバー呼び出しを実行し、最適化されたハッシュ関数を利用してパフォーマンスを向上させます。大規模ベンチマーク実験の結果、pactは従来方式よりも優れた性能向上を示した。たとえば、14,202個のインスタンスのうち、pactは603個を正常に処理したのに対し、既存の方式は13個のみを処理した。

Takeaways、Limitations

•
Takeaways：
◦
ハイブリッドSMT式のための効率的な近似モデル計数技術を提示
◦
ハッシュベースのアプローチにより、従来の方法よりもはるかに多くの問題を解決できます。
◦
理論的保証の下での近似モデルのカウント結果の提供
◦
大規模ベンチマーク実験による性能優秀性の検証
•
Limitations：
◦
近似モデルカウントなので正確な年数を保証しません。
◦
それでも多くのインスタンス（14,202個のうち13,600個以上）は解決できません。成功率がまだ低い。
👍
Made with Slashpage