ログイン
言語:

WEKO3

  • トップ
  • コミュニティ
  • ランキング
AND
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"}, "item_10_alternative_title_19": {"attribute_name": "\u305d\u306e\u4ed6\u306e\u8a00\u8a9e\u306e\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_alternative_title": "Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme"}]}, "item_10_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2011-10", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "268", "bibliographicPageEnd": "72", "bibliographicPageStart": "67", "bibliographicVolumeNumber": "111", "bibliographic_titles": [{"bibliographic_title": "\u96fb\u5b50\u60c5\u5831\u901a\u4fe1\u5b66\u4f1a\u6280\u8853\u7814\u7a76\u5831\u544a. SS, \u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u30b5\u30a4\u30a8\u30f3\u30b9"}]}]}, "item_10_description_4": {"attribute_name": "\u6284\u9332", "attribute_value_mlt": [{"subitem_description": "\u8ad6\u7406\u5f0f\u306e\u5145\u8db3\u53ef\u80fd\u6027\u5224\u5b9a\u554f\u984c(SAT\u554f\u984c)\u3092\u89e3\u304fSAT\u30bd\u30eb\u30d0\u306e\u9ad8\u901f\u5316\u306e\u4e00\u624b\u6cd5\u3068\u3057\u3066,\u99ac\u91ce\u3089\u306f2010\u5e74\u306bCNF\u3078\u306e\u57fa\u672c\u5bfe\u79f0\u7bc0\u306e\u5c0e\u5165\u3092\u63d0\u6848\u3057\u305f.\u5f7c\u3089\u306eSAT\u30bd\u30eb\u30d0\u306f,\u7bc0\u4e2d\u306e\u771f\u30ea\u30c6\u30e9\u30eb\u3068\u507d\u30ea\u30c6\u30e9\u30eb\u306e\u500b\u6570\u3092\u30ab\u30a6\u30f3\u30bf\u306b\u4fdd\u6301\u3059\u308b\u65b9\u6cd5\u306b\u3088\u308b\u5b9f\u73fe\u3067\u3042\u308b\u305f\u3081\u30d0\u30c3\u30af\u30c8\u30e9\u30c3\u30af\u304c\u91cd\u3044\u3068\u3044\u3046\u6b20\u70b9\u304c\u3042\u308b.\u305d\u3053\u3067, Minisat\u306b\u4ee3\u8868\u3055\u308c\u308b\u73fe\u5728\u4e3b\u6d41\u306e\u30bd\u30eb\u30d0\u304c\u63a1\u7528\u3059\u308b\u7bc0\u3042\u305f\u308a\u4e8c\u3064\u306e\u30ea\u30c6\u30e9\u30eb\u3092\u76e3\u8996\u3059\u308b\u65b9\u6cd5(2\u30ea\u30c6\u30e9\u30eb\u76e3\u8996\u6cd5)\u306b\u57fa\u3065\u304f\u5b9f\u73fe\u304c\u53ef\u80fd\u3067\u3042\u308c\u3070,\u30d0\u30c3\u30af\u30c8\u30e9\u30c3\u30af\u304c\u8efd\u304f\u306a\u308b\u305f\u3081\u66f4\u306a\u308b\u9ad8\u901f\u5316\u304c\u671f\u5f85\u3067\u304d\u308b.\u3057\u304b\u3057\u306a\u304c\u3089,\u57fa\u672c\u5bfe\u79f0\u7bc0\u306e\u6027\u8cea\u304b\u3089\u4e8c\u3064\u306e\u30ea\u30c6\u30e9\u30eb\u306e\u307f\u306e\u76e3\u8996\u3067\u306f\u5341\u5206\u3067\u306a\u304f,\u305d\u306e\u307e\u307e\u3067\u306f\u9ad8\u901f\u5316\u304c\u671f\u5f85\u3067\u304d\u306a\u3044.\u672c\u8ad6\u6587\u3067\u306f,\u901a\u5e38\u306e\u7bc0(OR\u7bc0)\u306f\u4e8c\u3064\u306e\u30ea\u30c6\u30e9\u30eb\u3092\u76e3\u8996\u3057,\u57fa\u672c\u5bfe\u79f0\u7bc0\u306b\u3064\u3044\u3066\u306f\u7bc0\u4e2d\u306e\u30ea\u30c6\u30e9\u30eb\u3092\u3059\u3079\u3066\u76e3\u8996\u3059\u308b\u65b9\u6cd5\u3092\u63d0\u6848\u3059\u308b,\u5b9f\u969b\u306b\u3053\u308c\u3092Minisat\u306b\u7d44\u307f\u8fbc\u3080\u3053\u3068\u3067,\u672c\u624b\u6cd5\u306e\u6709\u52b9\u6027\u3092\u8a55\u4fa1\u3059\u308b. 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_type": "Abstract"}]}, "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": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "\u4e00\u822c\u793e\u56e3\u6cd5\u4eba\u96fb\u5b50\u60c5\u5831\u901a\u4fe1\u5b66\u4f1a"}]}, "item_10_relation_40": {"attribute_name": "\u30b7\u30ea\u30fc\u30ba", "attribute_value_mlt": [{"subitem_relation_name": [{"subitem_relation_name_text": "IEICE Technical Report;SS2011-38"}]}]}, "item_10_select_15": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "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": "ISSN"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "\u65e5\u91ce, \u5584\u4fe1"}], "nameIdentifiers": [{"nameIdentifier": "62001", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u9152\u4e95, \u6b63\u5f66"}], "nameIdentifiers": [{"nameIdentifier": "62002", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u5742\u90e8, \u4fca\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "62003", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u8349\u5208, \u572d\u4e00\u6717"}], "nameIdentifiers": [{"nameIdentifier": "62004", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u897f\u7530, \u76f4\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "62005", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "HINO, Yoshizane"}], "nameIdentifiers": [{"nameIdentifier": "62006", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko"}], "nameIdentifiers": [{"nameIdentifier": "62007", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki"}], "nameIdentifiers": [{"nameIdentifier": "62008", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "KUSAKARI, Keiichirou"}], "nameIdentifiers": [{"nameIdentifier": "62009", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "NISHIDA, Naoki"}], "nameIdentifiers": [{"nameIdentifier": "62010", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "\u30d5\u30a1\u30a4\u30eb\u60c5\u5831", "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_free", "mimetype": "application/pdf", "size": 957300.0, "url": {"label": "110008900205.pdf", "url": "https://nagoya.repo.nii.ac.jp/record/21402/files/110008900205.pdf"}, "version_id": "d4e21a45-6e27-4c22-9295-0ec3ada15f84"}]}, "item_keyword": {"attribute_name": "\u30ad\u30fc\u30ef\u30fc\u30c9", "attribute_value_mlt": [{"subitem_subject": "SAT\u30bd\u30eb\u30d0", "subitem_subject_scheme": "Other"}, {"subitem_subject": "\u57fa\u672c\u5bfe\u79f0\u7bc0", "subitem_subject_scheme": "Other"}, {"subitem_subject": "2\u30ea\u30c6\u30e9\u30eb\u76e3\u8996\u6cd5", "subitem_subject_scheme": "Other"}, {"subitem_subject": "\u5168\u30ea\u30c6\u30e9\u30eb\u76e3\u8996\u6cd5", "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": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "2\u30ea\u30c6\u30e9\u30eb\u76e3\u8996\u6cd5\u3067\u5b9f\u88c5\u3055\u308c\u305fSAT\u30bd\u30eb\u30d0\u3078\u306e\u57fa\u672c\u5bfe\u79f0\u7bc0\u51e6\u7406\u6a5f\u80fd\u306e\u7d44\u307f\u8fbc\u307f", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "2\u30ea\u30c6\u30e9\u30eb\u76e3\u8996\u6cd5\u3067\u5b9f\u88c5\u3055\u308c\u305fSAT\u30bd\u30eb\u30d0\u3078\u306e\u57fa\u672c\u5bfe\u79f0\u7bc0\u51e6\u7406\u6a5f\u80fd\u306e\u7d44\u307f\u8fbc\u307f"}]}, "item_type_id": "10", "owner": "1", "path": ["312/313/314"], "permalink_uri": "http://hdl.handle.net/2237/23546", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "attribute_value": "2016-02-23"}, "publish_date": "2016-02-23", "publish_status": "0", "recid": "21402", "relation": {}, "relation_version_is_last": true, "title": ["2\u30ea\u30c6\u30e9\u30eb\u76e3\u8996\u6cd5\u3067\u5b9f\u88c5\u3055\u308c\u305fSAT\u30bd\u30eb\u30d0\u3078\u306e\u57fa\u672c\u5bfe\u79f0\u7bc0\u51e6\u7406\u6a5f\u80fd\u306e\u7d44\u307f\u8fbc\u307f"], "weko_shared_id": null}
  1. A500 情報学部/情報学研究科・情報文化学部・情報科学研究科
  2. A500a 雑誌掲載論文
  3. 学術雑誌

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

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ソルバへの基本対称節処理機能の組み込み
その他のタイトル
その他のタイトル Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme
著者 日野, 善信

× 日野, 善信

WEKO 62001

日野, 善信

Search repository
酒井, 正彦

× 酒井, 正彦

WEKO 62002

酒井, 正彦

Search repository
坂部, 俊樹

× 坂部, 俊樹

WEKO 62003

坂部, 俊樹

Search repository
草刈, 圭一朗

× 草刈, 圭一朗

WEKO 62004

草刈, 圭一朗

Search repository
西田, 直樹

× 西田, 直樹

WEKO 62005

西田, 直樹

Search repository
HINO, Yoshizane

× HINO, Yoshizane

WEKO 62006

HINO, Yoshizane

Search repository
SAKAI, Masahiko

× SAKAI, Masahiko

WEKO 62007

SAKAI, Masahiko

Search repository
SAKABE, Toshiki

× SAKABE, Toshiki

WEKO 62008

SAKABE, Toshiki

Search repository
KUSAKARI, Keiichirou

× KUSAKARI, Keiichirou

WEKO 62009

KUSAKARI, Keiichirou

Search repository
NISHIDA, Naoki

× NISHIDA, Naoki

WEKO 62010

NISHIDA, Naoki

Search repository
キーワード
主題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に組み込むことで,本手法の有効性を評価する. 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.
内容記述タイプ Abstract
出版者
出版者 一般社団法人電子情報通信学会
言語
言語 jpn
資源タイプ
資源タイプresource http://purl.org/coar/resource_type/c_6501
タイプ journal article
ISSN
収録物識別子タイプ ISSN
収録物識別子 0913-5685
書誌情報 電子情報通信学会技術研究報告. 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 CiteULike Twitter Facebook Print Addthis

Cite as

Export

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

Confirm


Powered by CERN Data Centre & Invenio


Powered by CERN Data Centre & Invenio