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