{"_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}