{"entities":{"Q543613":{"pageid":545380,"ns":120,"title":"Item:Q543613","lastrevid":62630271,"modified":"2026-04-11T07:23:09Z","type":"item","id":"Q543613","labels":{"en":{"language":"en","value":"On the power of clause-learning SAT solvers as resolution engines"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5909453"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$CA5C24CA-ED75-4958-AA95-BC99912A749A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b757bf3d14eb0f5f70b0e8db9cbb006a84072141","datavalue":{"value":{"text":"On the power of clause-learning SAT solvers as resolution engines","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q543613$C51A6124-8941-4793-B19A-0687385C2172","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e151c994012e6bc1d1ec4bc366518f4ccdcf0d4d","datavalue":{"value":"1216.68235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q543613$F5BD54B5-AEFD-4A8D-916A-933AF59AF32A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e8bf0e53587e1a257b0f354c5c435b9353c3c6b8","datavalue":{"value":{"entity-type":"item","numeric-id":543612,"id":"Q543612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$269DF31C-A749-4A23-8B46-1EF564DAE480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2ab581a8596fa2f5f17dcb9bcf516e7db4560e5f","datavalue":{"value":{"entity-type":"item","numeric-id":511783,"id":"Q511783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$BD523C30-B41A-48BD-8329-89C13C165EF9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"984e6510ec40a363d20e607cce2cc2f8b07918ae","datavalue":{"value":{"entity-type":"item","numeric-id":72340,"id":"Q72340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$72CF8EB8-A037-49C0-BB9A-82F970595944","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b7c5acb12eb16cd36e6bd9603815f2e919f7d5ec","datavalue":{"value":{"time":"+2011-06-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q543613$1315F026-9192-44AF-878F-9DFE2A31CAF1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q543613$7D810E9D-89C0-411F-9FC9-EFFC9E483DBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q543613$0C272CBB-32D6-4D6C-9B58-D36F8025C51E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bd120627ef5d2361e4b9c5cbb59e485196394940","datavalue":{"value":"5909453","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q543613$7D7AF173-6317-41D3-AEAE-92EF2916C191","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3978d2f31bc86b19c4025fe772ec1974bbd09669","datavalue":{"value":"Boolean satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q543613$8EA70C5B-59EB-46C3-B4E5-AC526C6FD3D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4cfa14d6edc9e16ee7b37b2f5389e8a53176bbc6","datavalue":{"value":"clause-learning SAT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q543613$0F29508E-B240-478C-BA1A-BB147B5943F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f7ac674268224c9b1b4b60f07b959745a70f08d","datavalue":{"value":"DPLL","type":"string"},"datatype":"string"},"type":"statement","id":"Q543613$41A2B329-2793-46B0-A2CF-684C17BDE015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q543613$21C3BD0E-10FB-4904-89C0-3A9CBC018E27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"80008d81258ded70d575e02944a82647618843a1","datavalue":{"value":"resolution proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q543613$62A58B5A-CF40-4ED4-8939-9AFC8B29AE2F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$917A68FD-18CD-4590-8408-19B8DB73A933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$93135336-3CCC-46F5-A0F7-87EFEE9448E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fc913e0e8afa2a727cce06bc306808aa43cd2398","datavalue":{"value":{"entity-type":"item","numeric-id":25035,"id":"Q25035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$7DED908B-37D4-415F-BA61-AC99B3373317","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f705e695e5daf5c1a4b07b9d249dfa9eda3d87b3","datavalue":{"value":{"entity-type":"item","numeric-id":16613,"id":"Q16613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$13D31AA7-5A48-43C1-8646-6DAA314A71CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"10ed1370106ab58118612ce8fef1abc06fcb61d2","datavalue":{"value":{"entity-type":"item","numeric-id":13776,"id":"Q13776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$6E57DAFA-B8B9-417A-BC18-4F2525321902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b029c35ffabe60b7d29584a6d40b4cb278ba542d","datavalue":{"value":{"entity-type":"item","numeric-id":18983,"id":"Q18983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$9FB7F9BC-A7C1-4553-BC10-A36463408FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"87d73f1b94c3ecc3f3dc21306b45943feea4ca05","datavalue":{"value":{"entity-type":"item","numeric-id":21465,"id":"Q21465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$F4C43C1A-CFE1-4740-80B6-57C5CDA95A54","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$430D88E1-58DD-4BEA-A050-65BC924896C3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"320f8207e686124207bb073766583aed42fc5a64","datavalue":{"value":"https://doi.org/10.1016/j.artint.2010.10.002","type":"string"},"datatype":"url"},"type":"statement","id":"Q543613$0148C30F-F88A-40E3-839D-A3D5D6B3F787","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9effe4877e2fdda4fdb4a3f62d2634885a70a9cf","datavalue":{"value":"W2121015471","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q543613$7541D9C9-98AA-45F4-A5F1-DBD386B5A664","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d99b374be2c44213411331fed2c8d045ed547272","datavalue":{"value":{"entity-type":"item","numeric-id":5902141,"id":"Q5902141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$8E08CD51-015A-4796-A9E9-727F7472720E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6ed378042883c33f78646cfc2e282152ec8d9f3","datavalue":{"value":{"entity-type":"item","numeric-id":3502689,"id":"Q3502689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$C6DCB342-5E72-4431-A875-8916F3DA2120","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"652707f3c517fc0bc45fb7ef7e533228515c0c0d","datavalue":{"value":{"entity-type":"item","numeric-id":5715680,"id":"Q5715680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$2AA14EF8-7687-425F-A583-2A0A7FB6A87A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08b529296035947435eb136154e374f9657d895b","datavalue":{"value":{"entity-type":"item","numeric-id":4406287,"id":"Q4406287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$2E0602FB-DDFB-498F-ADF1-82B82AE30D64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae8e8c7e4d2f66af1d6d76f2c025c2520cd9b217","datavalue":{"value":{"entity-type":"item","numeric-id":3623009,"id":"Q3623009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$ED86FE2E-033C-480C-B75D-A618C5CD9CCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$0D001C03-C13B-4E9B-A2E8-438415907EAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$C97ECADD-1F2C-4D37-9917-D23337BDB544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$30551876-8789-4938-8464-10A84695EF17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3348c4f23a620a7654545e9e3737b9f755ba6069","datavalue":{"value":{"entity-type":"item","numeric-id":2643301,"id":"Q2643301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$E2E6642A-2C1A-45B9-9908-056069457ADF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f34b98eb35b62210c470543927e38c2a7520c471","datavalue":{"value":{"entity-type":"item","numeric-id":689615,"id":"Q689615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$80FD1B9A-497E-4708-B909-D1BFCB1BA3D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a5f56faf1eb5778a67934d86dec7defa0e4c6f4","datavalue":{"value":{"entity-type":"item","numeric-id":5714769,"id":"Q5714769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$6A33F661-D5E0-46BC-8C7E-74869B9DF1D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$4F61AEAC-DE6C-43C6-9066-8F38EC18CFA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d75d3a49bdccbda045af07abb7b72f3249deadc","datavalue":{"value":{"entity-type":"item","numeric-id":5713713,"id":"Q5713713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$98D904C7-E3FC-4821-A4C4-F72271971DA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7e6dc1f84dd0187ce4214e5d421c9e0cb62a910","datavalue":{"value":{"entity-type":"item","numeric-id":5387867,"id":"Q5387867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q543613$F41FEAC4-E770-4A67-9942-17847091C465","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9c7026191b5ed0e000cb3c4823a24049f02bb43d","datavalue":{"value":"10.1016/J.ARTINT.2010.10.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q543613$D4D8132C-F624-4ED2-938E-B5866DFFF774","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e367b9365c51e5a796d1351242716e78cdb290d8","datavalue":{"value":{"entity-type":"item","numeric-id":5902141,"id":"Q5902141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6790ac591a93bbb144b604dec8633ea6754d5c2b","datavalue":{"value":{"amount":"+0.8659939169883728","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q543613$4BD24283-A297-4A02-B316-C558C83DAF0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e050f30d7185276802f36abdec5347610a74e3d","datavalue":{"value":{"entity-type":"item","numeric-id":5715680,"id":"Q5715680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7d0afc0470c44bdf921bb81bfe602e3ea2bc122","datavalue":{"value":{"amount":"+0.8620578050613403","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q543613$4F54401C-C157-4D64-9056-2B3F4D78D5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7d5c2eb27300f2b7854b64ee079eb9be89e6f87","datavalue":{"value":{"entity-type":"item","numeric-id":5894155,"id":"Q5894155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2cc214eadd03706f8237a8de697408aed18b59db","datavalue":{"value":{"amount":"+0.8530945181846619","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q543613$22942BCB-4877-4941-A5F6-D6E1F782C493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0aefed8d1dd77676745c8729f2c2484dc63de6d0","datavalue":{"value":{"entity-type":"item","numeric-id":622116,"id":"Q622116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e22915d0c8248a4f1eb27312759919894d83e8d","datavalue":{"value":{"amount":"+0.8445243239402771","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q543613$9EF6F39F-7149-465A-82D4-8502184C6265","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"227e1ab111833897f6610fc74feff763196614d2","datavalue":{"value":{"entity-type":"item","numeric-id":3007694,"id":"Q3007694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60cebe735f4393be0e1b1729b93b956caad5cdac","datavalue":{"value":{"amount":"+0.8206461071968079","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q543613$145858AB-1C26-43F1-AF47-A524C56DF850","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the power of clause-learning SAT solvers as resolution engines","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_power_of_clause-learning_SAT_solvers_as_resolution_engines"}}}}}