基本対称関数を付加したCNF論理式の充足可能性判定  [in Japanese] Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions  [in Japanese]

Search this Article

Author(s)

Abstract

近年,高速な充足可能性判定ツール(SATソルバ)の開発が進んでいる.これらのツールでは,変数値を次々に推論するBCPという演算がSATソルバの実行時間の大半を占めていることが多く,その処理を効率化できればSATソルバの高速化が可能となる.本論文では,「n個の変数のうち,ちょうどk個が真」という基本対称関数を導入することにより入力する論理式の大きさが減少することに注目し,SATソルバの効率化を目指す.実際にSATソルバでよく用いられるDLLアルゴリズムを基本対称関数を持つCNFに拡張し,その有効性を実験により確かめた.

In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed. Since BCP module, which propagates variable values in succession, often consumes most of running time of SAT solvers, the total efficiency will be improved if we succeed in reducing the process of BCP. In this paper, we attempt to improve the efficiency of SAT solvers from the observation that the number of clauses of a CNF formula is decreased by introducing the notion of elementary symmetric functions. We incorporated the notion into the DLL algorithm, implemented a SAT solver based on the extended algorithm and confirmed its effectiveness from experiments.

Journal

  • IEICE technical report

    IEICE technical report 108(362), 31-36, 2008-12-11

    The Institute of Electronics, Information and Communication Engineers

References:  16

Codes

  • NII Article ID (NAID)
    110007114884
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    9763798
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top