WEKO3
アイテム
Exploiting Functional Dependencies of Variables in All Solutions SAT Solvers
https://ipsj.ixsq.nii.ac.jp/records/182740
https://ipsj.ixsq.nii.ac.jp/records/182740deaae664-1921-428e-a10b-54321403283f
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JNL5807001.pdf (458.5 kB)
|
Copyright (c) 2017 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Journal(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2017-07-15 | |||||||||
| タイトル | ||||||||||
| タイトル | Exploiting Functional Dependencies of Variables in All Solutions SAT Solvers | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | Exploiting Functional Dependencies of Variables in All Solutions SAT Solvers | |||||||||
| 言語 | ||||||||||
| 言語 | eng | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [一般論文] AllSAT, model enumeration, OBDD compiler, functional dependency, independent variable | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| Graduate School of Informatics and Engineering, The University of Electro-Communications | ||||||||||
| 著者所属 | ||||||||||
| NTT Network Innovation Laboratories, NTT Corporation | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Informatics and Engineering, The University of Electro-Communications | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| NTT Network Innovation Laboratories, NTT Corporation | ||||||||||
| 著者名 |
Takahisa, Toda
× Takahisa, Toda
× Takeru, Inoue
|
|||||||||
| 著者名(英) |
Takahisa, Toda
× Takahisa, Toda
× Takeru, Inoue
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | All solutions SAT (AllSAT) is the problem of generating satisfying assignments to a given conjunctive normal form (CNF) and has been a key issue commonly found in several applications of formal verification including model checking. CNF encoding, which translates original problems for AllSAT solvers, spawns many auxiliary variables and, what is worse, obscures functional dependencies over variables. AllSAT solvers consequently have to deal with unnecessarily larger CNFs, although the original problems might be much more tractable in essence. This paper proposes a novel AllSAT solver along with a CNF encoding technique; our solver extracts functional dependencies through the encoding process, and the dependence is effectively utilized to solve the CNF. Our solver is designed based on the OBDD compilation technique, which allows us to efficiently handle intractable CNFs with a number of solutions in dynamic programming manner. Our proposal is very simple but powerful; experiments with real network instances showed that our solver exhibits a great improvement. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.25(2017) (online) DOI http://dx.doi.org/10.2197/ipsjjip.25.459 ------------------------------ |
|||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | All solutions SAT (AllSAT) is the problem of generating satisfying assignments to a given conjunctive normal form (CNF) and has been a key issue commonly found in several applications of formal verification including model checking. CNF encoding, which translates original problems for AllSAT solvers, spawns many auxiliary variables and, what is worse, obscures functional dependencies over variables. AllSAT solvers consequently have to deal with unnecessarily larger CNFs, although the original problems might be much more tractable in essence. This paper proposes a novel AllSAT solver along with a CNF encoding technique; our solver extracts functional dependencies through the encoding process, and the dependence is effectively utilized to solve the CNF. Our solver is designed based on the OBDD compilation technique, which allows us to efficiently handle intractable CNFs with a number of solutions in dynamic programming manner. Our proposal is very simple but powerful; experiments with real network instances showed that our solver exhibits a great improvement. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.25(2017) (online) DOI http://dx.doi.org/10.2197/ipsjjip.25.459 ------------------------------ |
|||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AN00116647 | |||||||||
| 書誌情報 |
情報処理学会論文誌 巻 58, 号 7, 発行日 2017-07-15 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7764 | |||||||||
