| 講演名 | 2003/6/11 論理式の解密度の濃縮 花谷 陽一, 堀山 貴史, 岩間 一雄, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 与えられた論理式&fnof:から別以下を満たす論理式gを生成する問題を考える。(1)&fnof:が充足不能ならばqも充足不能、(2)&fnof:が充足可能ならばqも充足可能で、qは&fnof:よりも"易しい"。我々は易しさの測度として、解の密度(充足解の個数/2^n)を定義する.ここでnは&fnof:の変数の個数を表す。本稿では、入力として与えられる論理式&fnof:を3-CNFであるとし、qを任意の論理演算を許した式とする。我々はこの問題に対し、2つの異なったアプローチをとる。ひとりは、変数を減らす方法で、もう一方は変数を増やす方法である。これらはそれぞれ既存のSATアルゴリズムに基づいている。我々の性能評価では、よりよいSATのアルゴリズムが、常によりよい密度の濃縮アルゴリズムを導出するわけではないことがわかった。 |
| 抄録(英) | The following problem is considered: Given a Boolean formula &fnof:, generate another formula q such that: (i)If &fnof: is unsatisfiable then q is also unsatisfiable. (ii) If &fnof: is satisfiable then q is also satisfiable and furthermore is "easier" than &fnof:. For the measure of this easiness, we use the density of a formula &fnof: which is defined as (the number of satisfying assignments) / 2^n, where n is the number of Boolean variables of &fnof:. In this paper, we mainly consider the case that the input formula &fnof: is given as a 3-CNF formula and the output formula q may be any formula using Boolean AND, OR and negation. Two different approaches to this problem are presented: One is to obtain q by reducing the number of variables and the other by increasing the number of variables, both of which are based on existing SAT algorithms. Our performance evaluation shows that, a little surprisingly, better SAT algorithms do not always give us better density-condensation algorithms. This is a preliminary report of the on-going research. |
| キーワード(和) | 論理式 / 充足可能性 / 計算量理論 |
| キーワード(英) | Boolean formulas / Satisfiability problems / Computational complexity |
| 資料番号 | COMP2003-20 |
| 発行日 |
| 研究会情報 | |
| 研究会 | COMP |
|---|---|
| 開催期間 | 2003/6/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Theoretical Foundations of Computing (COMP) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 論理式の解密度の濃縮 |
| サブタイトル（和） | |
| タイトル（英） | Density Condensation of Boolean Formulas |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 論理式 / Boolean formulas |
| キーワード(2)（和/英） | 充足可能性 / Satisfiability problems |
| キーワード(3)（和/英） | 計算量理論 / Computational complexity |
| 第 1 著者 氏名（和/英） | 花谷 陽一 / Yoichi HANATANI |
| 第 1 著者 所属（和/英） | 京都大学大学院情報学研究科 Graduate School of Informatics Kyoto University |
| 第 2 著者 氏名（和/英） | 堀山 貴史 / Takashi HORIYAMA |
| 第 2 著者 所属（和/英） | 京都大学大学院情報学研究科 Graduate School of Informatics Kyoto University |
| 第 3 著者 氏名（和/英） | 岩間 一雄 / Kazuo IWAMA |
| 第 3 著者 所属（和/英） | 京都大学大学院情報学研究科 Graduate School of Informatics Kyoto University |
| 発表年月日 | 2003/6/11 |
| 資料番号 | COMP2003-20 |
| 巻番号（vol） | vol.103 |
| 号番号（no） | 119 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |