{"entities":{"Q2405239":{"pageid":2415982,"ns":120,"title":"Item:Q2405239","lastrevid":52904525,"modified":"2026-01-23T18:56:40Z","type":"item","id":"Q2405239","labels":{"en":{"language":"en","value":"Satisfiability modulo theories and assignments"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6778396"}},"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":"Q2405239$5B8B4443-EB14-434A-AEC9-4EB38C5A0B36","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c93c2fdabc79f33d8b89cf01d2ed9ca3bd49fb8c","datavalue":{"value":{"text":"Satisfiability modulo theories and assignments","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2405239$07BD7C4A-35E2-45BA-91AF-F4195C6E61CA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3832f5864119ad50f5d3a4ab0c33f47a61025cd4","datavalue":{"value":"1468.68193","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405239$71BEA1A7-A8BD-4DF8-9D9F-D12EAD266820","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ffaf9228e2aed7473cbf6bedf4f944c34c643005","datavalue":{"value":"10.1007/978-3-319-63046-5_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405239$8BDB1C92-006C-4C5E-9F33-2F91FBEE770A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405239$CCDA3C6A-80E4-43F6-A2F4-4791E8B91A1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6be8d909a46685b6a24cecd253b3dd33cd2a6cb","datavalue":{"value":{"entity-type":"item","numeric-id":832718,"id":"Q832718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405239$730D6490-F9B3-4BE0-8DE5-21F9E3819FD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f977cc4afe30a7452131df7ff084411daffbbaa","datavalue":{"value":{"entity-type":"item","numeric-id":532428,"id":"Q532428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405239$C243772F-48AA-418B-85CC-620A233BC4F2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"75b8eddfcc302defc1a614ef0ded8c7b941f1ef4","datavalue":{"value":{"time":"+2017-09-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2405239$087D5A47-54AE-498B-99AD-F337A940FEB2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405239$516AE09A-2A95-4E35-BDA3-90E437896F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405239$43139FD3-1E1D-40F4-A7B3-6F20C23C56D4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"32d6ea122b0df7af7647d5004ec7e268bcc6d89b","datavalue":{"value":"6778396","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405239$526F631C-9A6B-4B52-B70B-B7C5622D7E50","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c97c87aad358aaa4a159991a487a984d3a19cc4","datavalue":{"value":"theory combination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2405239$B3AF79AA-B200-415F-B02C-00C93DEAA72F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba541055dc9223ac28a9cc043149f1fd4c5baf5e","datavalue":{"value":"conflict-driven decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2405239$966039F7-74C0-4C41-B189-693933E2D36B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b0133bb82e5a2899974ef5a92a207f1239299d2","datavalue":{"value":"model building","type":"string"},"datatype":"string"},"type":"statement","id":"Q2405239$54C4AF14-1A4A-4C31-BBF8-3416A5D25AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b395e8f6acd180e1625664cf0f73ca38f664e9d","datavalue":{"value":"satisfiability modulo assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q2405239$CB58BCA3-48A5-45B6-B57B-C872F0FA1C29","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":"Q2405239$2363CDBC-7FC2-4289-9EA3-A754D1706255","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"397788911785c3c798a47904a03b4a1f05739ee1","datavalue":{"value":"https://doi.org/10.1007/978-3-319-63046-5_4","type":"string"},"datatype":"url"},"type":"statement","id":"Q2405239$9CC0641D-7828-4EDE-812F-98EC5E0B255E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"de80ab295e6dfbee3b3ab96339e99db999ea2c34","datavalue":{"value":"W2729127299","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405239$9AE9F8DD-62A3-41AE-8A96-3C27DA9511BF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15687028d8b25ed5c6f15c20aca3938aac7bf34a","datavalue":{"value":{"entity-type":"item","numeric-id":2303254,"id":"Q2303254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d0311a77f716b766515fe4c92bec20f3a0357f3","datavalue":{"value":{"amount":"+0.8881899118423462","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":"Q2405239$7B6CDA64-C372-4FE8-90D3-A22D61056540","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663aa1de8a6d978e2db16aaa337bd4bfbec378db","datavalue":{"value":{"entity-type":"item","numeric-id":2185458,"id":"Q2185458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"798fa5ccf5f7545d34b00ddb19d31bc61362560d","datavalue":{"value":{"amount":"+0.8644682765007019","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":"Q2405239$F22EDA94-123A-4E7B-B590-2FE4D8C38C45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e71bfb5b68d2283442ce2c6ed865faa5ef3fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5756564,"id":"Q5756564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b72c762d79a161b4db2c61187b2939278536bafd","datavalue":{"value":{"amount":"+0.7936822175979614","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":"Q2405239$A18248B3-C98F-4B02-9469-73E609941742","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43b31fc71a6b23556d529814a409bb49f6e92fa7","datavalue":{"value":{"entity-type":"item","numeric-id":1853591,"id":"Q1853591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c14c1b8a7b2622e286da80b5ef75c5c36694c355","datavalue":{"value":{"amount":"+0.7826011180877686","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":"Q2405239$0BFE5E08-1C50-4260-B939-9E1FEDF819B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4091c7fc28b123a8b17ea655215cc991f1485b7","datavalue":{"value":{"entity-type":"item","numeric-id":4385440,"id":"Q4385440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e931ccb46734fe5a6be3f78c4ad815a0f59c4e34","datavalue":{"value":{"amount":"+0.7800742983818054","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":"Q2405239$A622CED6-103A-495D-9DED-9B893FE2BEEE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2405239","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2405239"}}}}}