{"entities":{"Q6082228":{"pageid":13216535,"ns":120,"title":"Item:Q6082228","lastrevid":38780804,"modified":"2024-12-16T11:05:08Z","type":"item","id":"Q6082228","labels":{"en":{"language":"en","value":"Generating Extended Resolution Proofs with a BDD-Based SAT Solver"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7760992"}},"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":"Q6082228$9A146B8B-52E2-4BF3-9EC6-AA7DAF7308F6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"328c34c154e04f82db3fb6356cce3d24b0a2a3b9","datavalue":{"value":{"text":"Generating Extended Resolution Proofs with a BDD-Based SAT Solver","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6082228$548E42E7-182D-420E-9AD5-2A7005AB46E8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4c0dfaf0fc788c819480eafe3d16472a4c34a567","datavalue":{"value":"10.1145/3595295","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6082228$01F1170A-E3B7-4368-9974-8B9AAC75D7E5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a2c27d3e0e0b5520ffb8ac40111c3ffad759a39f","datavalue":{"value":{"entity-type":"item","numeric-id":1426129,"id":"Q1426129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$2CC99720-091B-49FD-9167-EEE852B43521","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4545114e473836bad71ebea0181e527108d9e5ea","datavalue":{"value":{"entity-type":"item","numeric-id":352966,"id":"Q352966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$3A696076-0DB0-4D8F-A598-D6645EFB7A71","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ae5381e7211b64f5f54296c18dfaf60be613ba86","datavalue":{"value":{"entity-type":"item","numeric-id":2946565,"id":"Q2946565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$2FF0B0A5-AF0D-455D-825A-C365DA9453D8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2042b1414b93bc40245c70d5e20b5b936393c3d9","datavalue":{"value":{"time":"+2023-11-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6082228$65A1974A-D3CF-4CE4-A8A6-FE1002119EE8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6082228$63CA9CD5-AA56-451E-ABCD-783636668370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6082228$1B5C9318-D731-4913-90A3-80344BF51400","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6c0b3d621ebf7fe57d83e0d2bbee690465b9d946","datavalue":{"value":"7760992","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6082228$3017FB47-76C4-4A52-B116-5D31BBD48226","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3978d2f31bc86b19c4025fe772ec1974bbd09669","datavalue":{"value":"Boolean satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q6082228$EBF5F6E3-B5FA-4128-8258-B5ECD4F86196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bda86de3ee4e7c9902a8d526041721056eee9cf4","datavalue":{"value":"binary decision diagrams","type":"string"},"datatype":"string"},"type":"statement","id":"Q6082228$E9207B29-4A6E-44A9-8979-4A526A62915B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f0c23329b48b104ed3960c66a0cad0ccbc7b7f4","datavalue":{"value":"extended resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q6082228$21BD3315-0F77-4DBF-AAB7-E8AD9DF1B491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"341122506de1ac3ffe78cf6a3c74522be6cc2d36","datavalue":{"value":"Urquhart formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q6082228$45113864-8607-4EF7-8CAF-736B4F330689","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5dd39e62f874d4c5e47f6537f28ba248a212dfa5","datavalue":{"value":"mutilated chessboard","type":"string"},"datatype":"string"},"type":"statement","id":"Q6082228$4213685E-0BE2-4C38-BF64-3EF48AE8109B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da0e9d0620439bf34a43faa3e85c21c599fbb434","datavalue":{"value":"pigeonhole problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q6082228$3EA28807-5BEE-4E50-8DBB-372C96E900A9","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":"Q6082228$8DD6C430-B084-47E4-9B85-10E06B41393C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"969f22c2e1fcc10b1a49b07f05e049c2339de4a6","datavalue":{"value":{"entity-type":"item","numeric-id":1884991,"id":"Q1884991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$96AA5638-A9AB-47AD-8894-0D7E19320A71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5e59694ba693ed2b8af4b0c9c848f2b45a00bcf","datavalue":{"value":{"entity-type":"item","numeric-id":4817533,"id":"Q4817533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$23399EE1-EA73-4758-8016-5FA212BDACE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$83BD1DAE-FAA4-41EF-A11E-906C04B9372E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25ed20ca086ed8ee83e652195ddfbb40a6c734cb","datavalue":{"value":{"entity-type":"item","numeric-id":3176365,"id":"Q3176365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$EA5E7F66-4DB2-4362-8236-C129F70AF4BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2460d834fdbd5dfc5763b880e0a3eed5bed6624c","datavalue":{"value":{"entity-type":"item","numeric-id":2044191,"id":"Q2044191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$73AEF229-4789-4111-918A-8D65CE02C967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ac67e7445b37b0c19a3f9b56c95ac7b86ccf433","datavalue":{"value":{"entity-type":"item","numeric-id":2055876,"id":"Q2055876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$3E34C1B4-D2F8-41E2-9825-1250E3C7750E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf4fab5a4519bb0e4a7392865538dc50ad77fca2","datavalue":{"value":{"entity-type":"item","numeric-id":1193587,"id":"Q1193587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$DD236552-2554-4DC0-868D-2D1E3F6649D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62c9398475f7fa9379872481d74552458b55195f","datavalue":{"value":{"entity-type":"item","numeric-id":2723442,"id":"Q2723442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$76A5EC37-31B7-43D3-A96E-9BA5E9EF7921","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6e71078c0a1e40a18b75403dca73c6030ff790c","datavalue":{"value":{"entity-type":"item","numeric-id":2661327,"id":"Q2661327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$1C97D670-7F3F-45F5-BC70-944A62908081","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$6B17DE4E-55AB-4210-934D-2439727B62FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$F53122E1-5E15-432B-ACCE-2C3120978FEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e67fcddb24060125029173cfd968ce530b38d6ab","datavalue":{"value":{"entity-type":"item","numeric-id":1978379,"id":"Q1978379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$055A29CC-1A77-4011-B381-77D7A00B0A72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"778337e94fc24740160fe8c27efa4893aff163c0","datavalue":{"value":{"entity-type":"item","numeric-id":5325878,"id":"Q5325878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$3BDD24E0-F005-4019-A30E-DDDFDB6063E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8c3fb0ef3c7cbeb1b19e8a3632e3bd5fcfcda10","datavalue":{"value":{"entity-type":"item","numeric-id":1165257,"id":"Q1165257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$5604FF9B-37CD-4633-992E-8FC2011E4906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac0758251afe6a76a41e18f7daffbd45a12fb82b","datavalue":{"value":{"entity-type":"item","numeric-id":1408378,"id":"Q1408378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$7C8E6A91-47D5-4ABB-A5CF-C44AB672DE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$24BB3E52-8D9B-4821-8CFB-55FA75430CAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb401982c24cf60048aa19266cd42b3950ee7608","datavalue":{"value":{"entity-type":"item","numeric-id":5219922,"id":"Q5219922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$531FD94A-C02A-42AD-BA09-01A453E8D657","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd1ae1eae0bbb3048cc59d85f34aded019099780","datavalue":{"value":{"entity-type":"item","numeric-id":4928451,"id":"Q4928451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$E333E46C-2C99-4229-9620-6DEB944AD6F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca4be033dc1e037b43c1538205386964bc6ef38a","datavalue":{"value":{"entity-type":"item","numeric-id":3514498,"id":"Q3514498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$51A2E702-4CD0-4C9D-BA76-BD1352D3E95C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd73ca6e418060dc9aa1dc7053b40ae99fececfa","datavalue":{"value":{"entity-type":"item","numeric-id":5756562,"id":"Q5756562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$EDA35ECB-2507-4289-A85B-CFAA8EAEBE68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0d3508621c44cb1e31d1449d9069f4f0e7ae434","datavalue":{"value":{"entity-type":"item","numeric-id":1961452,"id":"Q1961452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$5844B084-7381-49F0-8C2D-88BF366DE508","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1951f16d4fe8a611f755a4887c35002e0149e28","datavalue":{"value":{"entity-type":"item","numeric-id":5919480,"id":"Q5919480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$55CD93A5-EC00-4658-94D9-FC2F1812313D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d04d3c5c4061c168377e8b976e916ba7fa84989","datavalue":{"value":{"entity-type":"item","numeric-id":1408382,"id":"Q1408382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$4F9522B9-D1F9-43B1-920C-1DC0007370A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbebee9b3fc070c9b73e7dd9a4fe191a6564e2bd","datavalue":{"value":{"entity-type":"item","numeric-id":4071451,"id":"Q4071451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$51F7CD0A-EEB2-4795-AA70-F969D0487672","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73f9a6c4f4bcee377c44fbafa74bfc3c8af5729c","datavalue":{"value":{"entity-type":"item","numeric-id":5714754,"id":"Q5714754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$9911E16D-B4C3-4ECC-8CBC-4234F0417940","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0b58d0abcd9e4d9a58c0a0e5204160a728cc8f","datavalue":{"value":{"entity-type":"item","numeric-id":4645727,"id":"Q4645727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$E8A7801A-065F-43D8-98CF-8E8D8F955879","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":"Q6082228$A0EF850E-D496-49EF-8C72-F20E7FB6C613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b107d69d8ca98db7620611ee6ace5f0ce2d290cb","datavalue":{"value":{"entity-type":"item","numeric-id":3524229,"id":"Q3524229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$E48CE130-1F32-4E5F-BB3B-CC4F123A2D01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a75db9bdf4ecf4e316a158af7db19da7d850d73","datavalue":{"value":{"entity-type":"item","numeric-id":3434726,"id":"Q3434726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$3F46AA9F-346D-46F2-A916-51151EFC434B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e99741ea86af8e3fe4690d90c224835231a7ef4d","datavalue":{"value":{"entity-type":"item","numeric-id":2233509,"id":"Q2233509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$2A131CED-0749-48C0-A9E2-0ED79583CFC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b7519aefa4dda7e919ee4a80b4ac0ff9a83e620","datavalue":{"value":{"entity-type":"item","numeric-id":5096299,"id":"Q5096299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$421C685B-E772-45FD-AC3B-BD3E53A08C21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acddcbbc7bbb65cd6789ce6d861571f4cbd168d8","datavalue":{"value":{"entity-type":"item","numeric-id":4873893,"id":"Q4873893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$5A6BFA7E-1CDF-4755-BE11-9F48F0A41574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"871a7838603e3c550db89a4460c5c1dba9e680e8","datavalue":{"value":{"entity-type":"item","numeric-id":694550,"id":"Q694550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$CC400611-0970-4841-B74B-67E952F52374","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c38972f0f758fc01d3439768de6ed419c5d165d0","datavalue":{"value":{"entity-type":"item","numeric-id":3507034,"id":"Q3507034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$43687272-28AA-4BB4-835C-67431C55B086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb081c24d3f308759ffc5be25d93bb06a52b464f","datavalue":{"value":{"entity-type":"item","numeric-id":3192088,"id":"Q3192088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6082228$97CBD8ED-74FB-466F-8D2E-47279AE55D22","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ca9c4143e82164a915f320431c6c3d92a5f1d0f5","datavalue":{"value":"Q130888011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6082228$52BB366E-7796-4208-AB82-FFCBC4BD8946","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6082228","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6082228"}}}}}