ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

{"_buckets": {"deposit": "9df12941-8c1e-4b69-87f4-767609dac0a8"}, "_deposit": {"id": "21402", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "21402"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00021402", "sets": ["314"]}, "author_link": ["62001", "62002", "62003", "62004", "62005", "62006", "62007", "62008", "62009", "62010"], "item_10_alternative_title_19": {"attribute_name": "その他のタイトル", "attribute_value_mlt": [{"subitem_alternative_title": "Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme", "subitem_alternative_title_language": "en"}]}, "item_10_biblio_info_6": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2011-10", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "268", "bibliographicPageEnd": "72", "bibliographicPageStart": "67", "bibliographicVolumeNumber": "111", "bibliographic_titles": [{"bibliographic_title": "電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス", "bibliographic_titleLang": "ja"}]}]}, "item_10_description_4": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "論理式の充足可能性判定問題(SAT問題)を解くSATソルバの高速化の一手法として,馬野らは2010年にCNFへの基本対称節の導入を提案した.彼らのSATソルバは,節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある.そこで, Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法(2リテラル監視法)に基づく実現が可能であれば,バックトラックが軽くなるため更なる高速化が期待できる.しかしながら,基本対称節の性質から二つのリテラルのみの監視では十分でなく,そのままでは高速化が期待できない.本論文では,通常の節(OR節)は二つのリテラルを監視し,基本対称節については節中のリテラルをすべて監視する方法を提案する,実際にこれをMinisatに組み込むことで,本手法の有効性を評価する. ", "subitem_description_language": "ja", "subitem_description_type": "Abstract"}, {"subitem_description": "Umano et al. introduced elementary symmetric clauses (ES-clauses) into CNF formula in 2010 as a method for improving SAT-solver efficiency. Since their experimental SAT solver is implemented based on two counters that maintain the number of true (false, respectively) literals, it has a drawback that backtracks are heavy. Thus much faster solvers are expected due to light backtracks if it is possible to implement them based on watching two literals for each clause, called two watched literals adopted by modern SAT solvers like Minisat. However, watching two literals for ES-clauses are not enough for efficiency. This paper proposes a method watching two literals for each ordinary clause and watching all literals for each ES-clause, and evaluates this by incorporating it into Minisat.", "subitem_description_language": "en", "subitem_description_type": "Abstract"}]}, "item_10_description_5": {"attribute_name": "内容記述", "attribute_value_mlt": [{"subitem_description": "IEICE Technical Report;SS2011-38", "subitem_description_language": "en", "subitem_description_type": "Other"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "URI", "subitem_identifier_uri": "http://ci.nii.ac.jp/naid/110008900205/"}, {"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/23546"}]}, "item_10_publisher_32": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "一般社団法人電子情報通信学会", "subitem_publisher_language": "ja"}]}, "item_10_relation_40": {"attribute_name": "シリーズ", "attribute_value_mlt": [{"subitem_relation_name": [{"subitem_relation_name_text": "IEICE Technical Report;SS2011-38"}]}]}, "item_10_relation_43": {"attribute_name": "関連情報", "attribute_value_mlt": [{"subitem_relation_type": "isVersionOf", "subitem_relation_type_id": {"subitem_relation_type_id_text": "http://ci.nii.ac.jp/naid/110008900205/", "subitem_relation_type_select": "URI"}}]}, "item_10_select_15": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_10_source_id_7": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0913-5685", "subitem_source_identifier_type": "PISSN"}]}, "item_1615787544753": {"attribute_name": "出版タイプ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_970fb48d4fbd8a85", "subitem_version_type": "VoR"}]}, "item_access_right": {"attribute_name": "アクセス権", "attribute_value_mlt": [{"subitem_access_right": "open access", "subitem_access_right_uri": "http://purl.org/coar/access_right/c_abf2"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "日野, 善信", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "62001", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "酒井, 正彦", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "62002", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "坂部, 俊樹", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "62003", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "草刈, 圭一朗", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "62004", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "西田, 直樹", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "62005", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "HINO, Yoshizane", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "62006", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "62007", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "62008", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "KUSAKARI, Keiichirou", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "62009", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "NISHIDA, Naoki", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "62010", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-01-01"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "110008900205.pdf", "filesize": [{"value": "957.3 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 957300.0, "url": {"label": "110008900205.pdf", "objectType": "fulltext", "url": "https://nagoya.repo.nii.ac.jp/record/21402/files/110008900205.pdf"}, "version_id": "d4e21a45-6e27-4c22-9295-0ec3ada15f84"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "SATソルバ", "subitem_subject_scheme": "Other"}, {"subitem_subject": "基本対称節", "subitem_subject_scheme": "Other"}, {"subitem_subject": "2リテラル監視法", "subitem_subject_scheme": "Other"}, {"subitem_subject": "全リテラル監視法", "subitem_subject_scheme": "Other"}, {"subitem_subject": "SAT solver", "subitem_subject_scheme": "Other"}, {"subitem_subject": "elementary symmetric clauses", "subitem_subject_scheme": "Other"}, {"subitem_subject": "two watched literals", "subitem_subject_scheme": "Other"}, {"subitem_subject": "all watched literals", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み", "subitem_title_language": "ja"}]}, "item_type_id": "10", "owner": "1", "path": ["314"], "permalink_uri": "http://hdl.handle.net/2237/23546", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2016-02-23"}, "publish_date": "2016-02-23", "publish_status": "0", "recid": "21402", "relation": {}, "relation_version_is_last": true, "title": ["2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み"], "weko_shared_id": -1}
  1. A500 情報学部/情報学研究科・情報文化学部・情報科学研究科
  2. A500a 雑誌掲載論文
  3. 学術雑誌

2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み

http://hdl.handle.net/2237/23546
http://hdl.handle.net/2237/23546
f1d71a42-77a0-44d8-9d28-3e701f05bb73
名前 / ファイル ライセンス アクション
110008900205.pdf 110008900205.pdf (957.3 kB)
Item type 学術雑誌論文 / Journal Article(1)
公開日 2016-02-23
タイトル
タイトル 2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み
言語 ja
その他のタイトル
その他のタイトル Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme
言語 en
著者 日野, 善信

× 日野, 善信

WEKO 62001

ja 日野, 善信

Search repository
酒井, 正彦

× 酒井, 正彦

WEKO 62002

ja 酒井, 正彦

Search repository
坂部, 俊樹

× 坂部, 俊樹

WEKO 62003

ja 坂部, 俊樹

Search repository
草刈, 圭一朗

× 草刈, 圭一朗

WEKO 62004

ja 草刈, 圭一朗

Search repository
西田, 直樹

× 西田, 直樹

WEKO 62005

ja 西田, 直樹

Search repository
HINO, Yoshizane

× HINO, Yoshizane

WEKO 62006

en HINO, Yoshizane

Search repository
SAKAI, Masahiko

× SAKAI, Masahiko

WEKO 62007

en SAKAI, Masahiko

Search repository
SAKABE, Toshiki

× SAKABE, Toshiki

WEKO 62008

en SAKABE, Toshiki

Search repository
KUSAKARI, Keiichirou

× KUSAKARI, Keiichirou

WEKO 62009

en KUSAKARI, Keiichirou

Search repository
NISHIDA, Naoki

× NISHIDA, Naoki

WEKO 62010

en NISHIDA, Naoki

Search repository
アクセス権
アクセス権 open access
アクセス権URI http://purl.org/coar/access_right/c_abf2
キーワード
主題Scheme Other
主題 SATソルバ
キーワード
主題Scheme Other
主題 基本対称節
キーワード
主題Scheme Other
主題 2リテラル監視法
キーワード
主題Scheme Other
主題 全リテラル監視法
キーワード
主題Scheme Other
主題 SAT solver
キーワード
主題Scheme Other
主題 elementary symmetric clauses
キーワード
主題Scheme Other
主題 two watched literals
キーワード
主題Scheme Other
主題 all watched literals
抄録
内容記述 論理式の充足可能性判定問題(SAT問題)を解くSATソルバの高速化の一手法として,馬野らは2010年にCNFへの基本対称節の導入を提案した.彼らのSATソルバは,節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある.そこで, Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法(2リテラル監視法)に基づく実現が可能であれば,バックトラックが軽くなるため更なる高速化が期待できる.しかしながら,基本対称節の性質から二つのリテラルのみの監視では十分でなく,そのままでは高速化が期待できない.本論文では,通常の節(OR節)は二つのリテラルを監視し,基本対称節については節中のリテラルをすべて監視する方法を提案する,実際にこれをMinisatに組み込むことで,本手法の有効性を評価する.
言語 ja
内容記述タイプ Abstract
抄録
内容記述 Umano et al. introduced elementary symmetric clauses (ES-clauses) into CNF formula in 2010 as a method for improving SAT-solver efficiency. Since their experimental SAT solver is implemented based on two counters that maintain the number of true (false, respectively) literals, it has a drawback that backtracks are heavy. Thus much faster solvers are expected due to light backtracks if it is possible to implement them based on watching two literals for each clause, called two watched literals adopted by modern SAT solvers like Minisat. However, watching two literals for ES-clauses are not enough for efficiency. This paper proposes a method watching two literals for each ordinary clause and watching all literals for each ES-clause, and evaluates this by incorporating it into Minisat.
言語 en
内容記述タイプ Abstract
内容記述
内容記述 IEICE Technical Report;SS2011-38
言語 en
内容記述タイプ Other
出版者
言語 ja
出版者 一般社団法人電子情報通信学会
言語
言語 jpn
資源タイプ
資源タイプresource http://purl.org/coar/resource_type/c_6501
タイプ journal article
出版タイプ
出版タイプ VoR
出版タイプResource http://purl.org/coar/version/c_970fb48d4fbd8a85
関連情報
関連タイプ isVersionOf
識別子タイプ URI
関連識別子 http://ci.nii.ac.jp/naid/110008900205/
ISSN
収録物識別子タイプ PISSN
収録物識別子 0913-5685
書誌情報 ja : 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス

巻 111, 号 268, p. 67-72, 発行日 2011-10
著者版フラグ
値 publisher
シリーズ
関連名称 IEICE Technical Report;SS2011-38
URI
識別子 http://ci.nii.ac.jp/naid/110008900205/
識別子タイプ URI
URI
識別子 http://hdl.handle.net/2237/23546
識別子タイプ HDL
戻る
0
views
See details
Views

Versions

Ver.1 2021-03-01 15:23:56.086351
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3