{"entities":{"Q2996914":{"pageid":3007638,"ns":120,"title":"Item:Q2996914","lastrevid":58097166,"modified":"2026-04-03T19:14:10Z","type":"item","id":"Q2996914","labels":{"en":{"language":"en","value":"Computing small unsatisfiable cores in satisfiability modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5883660"}},"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":"Q2996914$D55584EB-A087-46E3-98DA-43DCB7A1C486","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8a6ef48d19de399aab59f0ae0ba5e5033c5e6f17","datavalue":{"value":{"text":"Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2996914$38187D56-A71B-4F29-B398-B359019B82E1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c5123d5a216723cfb14b60dcee57fec268bbdd94","datavalue":{"value":"1216.68241","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$35933C62-C833-4C50-94A8-439AD565FB61","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"387e6ac60ed3a0144bb303179c23c53493d401d0","datavalue":{"value":{"entity-type":"item","numeric-id":329418,"id":"Q329418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$6D66F151-BDED-4C9A-A060-8D9552212806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97e7d65eece04188cb1a1dff66ddc09c38fbea4","datavalue":{"value":{"entity-type":"item","numeric-id":479835,"id":"Q479835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$25716A46-534C-4784-ADF4-6D471A6CE05E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4fd5a076641129df5baba24779caed9dec893447","datavalue":{"value":{"entity-type":"item","numeric-id":511776,"id":"Q511776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$193901A0-E7A5-4B95-BCBD-7B08759416EC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb469f8c3341c58b96368431d3c87cbee3d3281e","datavalue":{"value":{"entity-type":"item","numeric-id":110835,"id":"Q110835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$86F1D0D6-995C-4815-BE89-BBE75C5B903D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8e8cf336a281775d77f65d41085e5a0ff9f89f4f","datavalue":{"value":{"time":"+2011-05-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":"Q2996914$492656A6-64C6-4416-B108-405F0B304D76","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"21d823e612f9525eebd146a13111effb74b84904","datavalue":{"value":"https://arxiv.org/abs/1401.3878","type":"string"},"datatype":"url"},"type":"statement","id":"Q2996914$A2E70A3C-671A-4921-9748-B8BE9A0FFF02","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$E28A74DD-82EB-4130-930C-B7941CC38A1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$8C2F1FA2-8D94-4092-A1DB-1F8159DB6197","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"09cf1042e216007a4f311e43e2ea9b1d46ca8c50","datavalue":{"value":"5883660","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$0E0B981E-8B22-4FB2-A810-7813B6D5BE29","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75999b4145baf8e36d1aae9da7d6c1e17358728e","datavalue":{"value":"satisfiability modulo theories (SMT)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2996914$879A7D11-672E-4ACF-9DD3-A710F2FBF036","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"096ae13994bb399733f2ba05424a6c86d46f8e92","datavalue":{"value":"Lemma-Lifting","type":"string"},"datatype":"string"},"type":"statement","id":"Q2996914$11E5ACD0-0C40-4B2F-8D5D-472E0337DAD3","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"5ac288a8efc7ac7a705cb1312dd3c9cda2d822cc","datavalue":{"value":"Q62041217","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$EA00C4EE-4ACB-49E8-B07C-347F9084BF06","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$A523D4FB-AF5C-4103-8C24-6DE46B138B8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$E5A4A6FF-3185-467C-8C0C-8B6F5CD712CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"60c977c73f66c80db6a0782a3e55d401ee00ddc1","datavalue":{"value":{"entity-type":"item","numeric-id":19150,"id":"Q19150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$52B1ADE1-074F-4C32-85C9-4F5A95B6F4AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9610c11cc8a90dd542e7dbbf77c0e56d86b59abe","datavalue":{"value":{"entity-type":"item","numeric-id":23846,"id":"Q23846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$6F6DDD00-42CC-4029-AC22-14944DABD078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b7940ddd2cf390857912577a8a65fd86fda5b260","datavalue":{"value":{"entity-type":"item","numeric-id":23851,"id":"Q23851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2996914$EBAD007B-D916-483A-A852-6370F0D7721A","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":"Q2996914$D2E78640-CFC5-419C-89AD-EE125DD77C3E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"356f2c1ebf5c16bde83043d5c113495d715ec7a9","datavalue":{"value":"W1775889152","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$3E3A1116-86D0-475F-9F83-EB699E7E7414","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f2ed46f6fb1d51f8bfcf602ddcec6c9462ee16a3","datavalue":{"value":"10.1613/JAIR.3196","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2996914$CDD0E677-E30C-4A82-957D-819A28C3A985","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48f2f1bc8aa3afbb16568e931cc28ee9326b5225","datavalue":{"value":{"entity-type":"item","numeric-id":3612475,"id":"Q3612475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"420e589e05a8c6aca6dd914032f308acf0014636","datavalue":{"value":{"amount":"+0.9353320002555848","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":"Q2996914$17F3B335-19DD-4236-94CE-E72C7C9265BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8baa14e88319bb40aae8bb111e040434ebce5abb","datavalue":{"value":{"entity-type":"item","numeric-id":3007682,"id":"Q3007682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24d5dcc8460fff65b792af4de5db994c9fe65eca","datavalue":{"value":{"amount":"+0.7996245622634888","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":"Q2996914$0E68B855-2024-42AD-8A03-B73917E9CF4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e7096f47b9d27f8c1e87f020fcdf13208c9657ba","datavalue":{"value":{"entity-type":"item","numeric-id":1028724,"id":"Q1028724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"200a4177a59922eda7523e31aa21c57910884830","datavalue":{"value":{"amount":"+0.7957573533058167","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":"Q2996914$7ABD43BE-087B-4CDE-BD62-7460575A93D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"305314cd53c45094fbe0975e30108a02ae33267c","datavalue":{"value":{"entity-type":"item","numeric-id":5756585,"id":"Q5756585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da438f60871abbada08bdc3af0ab9f2a4fc94d1c","datavalue":{"value":{"amount":"+0.7867802977561951","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":"Q2996914$CF4B4C86-5B95-43D3-BF39-ECADDFD43E91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a30b4d55194d040fcea1595b87e24275e383b833","datavalue":{"value":{"entity-type":"item","numeric-id":3400917,"id":"Q3400917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ceeca5dc62433a9a60022586e74a1c066a29e97","datavalue":{"value":{"amount":"+0.7714120745658875","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":"Q2996914$3A7C643C-10DC-4708-AB2B-F32044C4B7FE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2996914","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2996914"}}}}}