{"entities":{"Q2044191":{"pageid":2054933,"ns":120,"title":"Item:Q2044191","lastrevid":57710466,"modified":"2026-04-01T00:56:38Z","type":"item","id":"Q2044191","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 7378298"}},"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":"Q2044191$52DC5884-D801-4011-8E07-F4B68EA9961E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"90c0b388404d29e34236f453b02f5738643f27f6","datavalue":{"value":{"text":"Generating extended resolution proofs with a BDD-based SAT solver","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2044191$3BBDB2DF-7B14-43E5-8512-72AF9E715158","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e1a20f15f26ad326d336a6a44e5b713710e0cc11","datavalue":{"value":"1467.68203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$59E85A55-9F3F-44E6-ACBF-3CAD47875222","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3dda19f020c963d3372ae0d1ce779756df365a56","datavalue":{"value":"10.1007/978-3-030-72016-2_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$2A7CD60A-C580-4176-BC05-74B39BC8503F","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":"Q2044191$044607AC-0A99-465C-9229-17FE0C852988","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":"Q2044191$017E6AA6-B2B1-40BE-9E8F-7E4596582746","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6f25f924676185979ab6f246b476dde833797f44","datavalue":{"value":{"time":"+2021-08-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2044191$D2DDC5FE-26F8-431E-9B07-B4256F5A46FF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b90c0cdc753eeb2d9b202995c51ee41542f403b1","datavalue":{"value":"https://arxiv.org/abs/2105.00885","type":"string"},"datatype":"url"},"type":"statement","id":"Q2044191$40922BB7-C5D7-4E4F-A0A9-7EBDE228C76E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$27424572-DF7E-4B31-842F-84A6289C3B5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$A7B7FF69-ED33-4A00-B562-9BAC4BBE18BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$FCEC00BD-48FA-4072-88A1-BDCDA0C23AB8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e67685425b5aa0b9f0395b753e5a0d2a8bb93662","datavalue":{"value":"7378298","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$F24B7391-8CB8-4056-93C6-93D2D5EAEB77","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f0c23329b48b104ed3960c66a0cad0ccbc7b7f4","datavalue":{"value":"extended resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044191$41D6E76B-6C64-4AD4-8B3A-1C99F3E3E230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bda86de3ee4e7c9902a8d526041721056eee9cf4","datavalue":{"value":"binary decision diagrams","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044191$E2222729-CC00-4741-B1E0-795DCDA5103B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5dd39e62f874d4c5e47f6537f28ba248a212dfa5","datavalue":{"value":"mutilated chessboard","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044191$38A9DAB4-3CB8-443B-B38B-99143BC3095E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da0e9d0620439bf34a43faa3e85c21c599fbb434","datavalue":{"value":"pigeonhole problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044191$053B9D27-AAF1-471A-AD63-364A66F8AF26","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":"Q2044191$BCAE7003-5414-4FE3-B6A6-63BE488C948D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4f34b3f3b7fd703491075b44d6acc32702fb9090","datavalue":{"value":"W3136791784","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044191$6CD77AD2-D1B8-44AB-B340-BB2B30DC8F1B","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":"Q2044191$CC5F3EEA-3997-488D-BD7D-CB85B715D620","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":"Q2044191$39D52664-CF8D-49A6-8BA7-B0FE96B41CE7","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":"Q2044191$210949D8-53CD-456C-AA62-0F73A6081798","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":"Q2044191$404AAF69-E7DA-4A19-9498-2F35C65F118E","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":"Q2044191$B09787BB-DC0A-4A21-A52D-98C38C697D27","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":"Q2044191$9B0EE406-7467-424F-967B-73EA2D00AFA5","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":"Q2044191$D8B541AE-B935-4E44-A429-B59809997D9B","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":"Q2044191$37784D1A-E827-45F3-8745-71EAC7D683D9","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":"Q2044191$8A451041-FC97-40B8-AB6A-98D8EBD5FF95","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":"Q2044191$F792D6CC-9CB6-4DB7-AFD5-231028323F8F","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":"Q2044191$7368E57D-7668-423B-9C5E-7A79C86881CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9787938b4bdd367ccabbe7faf36857ca182203e7","datavalue":{"value":{"entity-type":"item","numeric-id":2324225,"id":"Q2324225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044191$6DA07970-FE91-4E7C-9C5C-A9C0CD6A6E4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d43182de98d159f0ebb543c5126e0ae385036ba","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044191$CC6C9CBF-1C9F-41D7-9D6D-C40C55ED75E3","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":"Q2044191$62D47311-2AF5-4095-BA74-5B090E038FDD","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":"Q2044191$172B9DBC-C471-4E0B-B4B3-FB1577DAB813","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":"Q2044191$F4DC2CD0-D387-436C-82EB-3E3CE000B5D0","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":"Q2044191$B15A6BD0-6481-473A-9436-955FF1AFD807","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":"Q2044191$7A82FD4B-F6D9-4BFD-941B-B5B04FC5AD8F","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":"Q2044191$75C09D5F-C4D8-4423-97B5-F5E21E5CE814","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":"Q2044191$BA0AAAD9-01DD-47EC-86CA-162F8C3B0704","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2caf86375d5742ea2c000a772a856d31236b04b6","datavalue":{"value":{"entity-type":"item","numeric-id":3682462,"id":"Q3682462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044191$B705B181-2591-4E89-BD53-95AAC78F3E7A","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":"Q2044191$CDF3EC29-A520-40BE-9978-C3AEA58ECD59","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":"Q2044191$CC7D1D60-C8BF-44ED-8A42-7DDC2EB9B23C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86572fb6fb3c840ab9b63220bf0ccf1b10386756","datavalue":{"value":{"entity-type":"item","numeric-id":3434726,"id":"Q3434726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"acd79d22d0f73f635eaad6e1ee06744170ff137c","datavalue":{"value":{"amount":"+0.8548945188522339","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":"Q2044191$55876465-E4D9-4051-A9E9-F6F9C2B769E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ceb101889724353cd33618c660b8363d0833f238","datavalue":{"value":{"entity-type":"item","numeric-id":5756562,"id":"Q5756562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09ea560a40f98ce762a9455cbad857d78a9b2f08","datavalue":{"value":{"amount":"+0.8452883362770081","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":"Q2044191$44DF7C8A-D702-4147-A08A-C00D61D510BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38ca28bbd0026f0ab61292d39747a92f0976141a","datavalue":{"value":{"entity-type":"item","numeric-id":2478427,"id":"Q2478427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"659542ed27906b748835a04079bed619aebd04fd","datavalue":{"value":{"amount":"+0.7924579977989197","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":"Q2044191$D902759F-2308-4085-B279-92D236A8DA3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32781204d1db0d50f0fed8e58f21ef2e924a069d","datavalue":{"value":{"entity-type":"item","numeric-id":5327347,"id":"Q5327347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80bbe0828cb66c47e00cf44bef7f407b10c0c5b3","datavalue":{"value":{"amount":"+0.7536184787750244","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":"Q2044191$CC254190-0692-4DEE-A31E-41C65A591C31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8de78b6076dabd1a68c913f5338b22a8d693321","datavalue":{"value":{"entity-type":"item","numeric-id":4928451,"id":"Q4928451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8edeafad18493e0039658a13bb14b63422261301","datavalue":{"value":{"amount":"+0.7535919547080994","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":"Q2044191$92CEC39B-D25E-4BEF-8D16-1E6A2694E50B","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044191$914C88A8-C0D9-40B7-924B-63FC747368FF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2044191","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2044191"}}}}}