{"entities":{"Q2961575":{"pageid":2972300,"ns":120,"title":"Item:Q2961575","lastrevid":52748396,"modified":"2026-01-23T10:22:43Z","type":"item","id":"Q2961575","labels":{"en":{"language":"en","value":"Solving nonlinear integer arithmetic with MCSAT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6687364"}},"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":"Q2961575$FF6FB9D6-A385-4570-A85B-7BC4DBE2D33E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"77cc46fa3646d6af9f799047d40aa43ccefd6f9f","datavalue":{"value":{"text":"Solving Nonlinear Integer Arithmetic with MCSAT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2961575$F88329B5-7523-46A2-A182-93261BA6311D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2bdf581b77b7586376c65be201d792b8fa08815a","datavalue":{"value":"1484.68220","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2961575$15211CFE-E0CD-4399-A801-158A2E76A6E0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"50e97b074fa41af450d967a82f69da79c427b5db","datavalue":{"value":"10.1007/978-3-319-52234-0_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2961575$3F8E675F-2B71-442F-97B7-EBBD5B59B707","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"397d77ad8bd1a3f514ce08804fba49d28413c3f4","datavalue":{"value":{"entity-type":"item","numeric-id":832266,"id":"Q832266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$647E64EA-93BE-4433-BF40-50DA5B746DE2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$305664D4-FF81-4B82-8F8E-C99FBFECC7B2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2fd8f9c1001071b6cee894af884cbd2ca840dd53","datavalue":{"value":{"time":"+2017-02-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2961575$17340798-CF66-4879-B582-7BE65217212C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2961575$2BEC10DF-8B7C-40D0-BEB4-36C841E1AAD1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ec2d3fe1cbc8a28edaadd333aab66baa8f63e4e2","datavalue":{"value":"6687364","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2961575$91FE0C6D-1CEC-4D3E-A03D-9BD368CD6B58","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"352070f92a42ab6c0ae16e5d77d8a717bc392ccc","datavalue":{"value":{"entity-type":"item","numeric-id":19847,"id":"Q19847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$65D80CED-4D73-4AD0-8D61-2B161090C378","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$E6E563DD-D6EE-4323-89EB-4C4720188E37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$8E8A0824-2636-4676-A07E-87C874501CD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$1C901545-8947-4120-A06A-BDF59CEFF488","rank":"normal"},{"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":"Q2961575$94F10A37-3AA6-485E-9F70-CC1E045E5993","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":"Q2961575$D04D0001-CB3D-4C0F-B77B-79F1FC396322","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":"Q2961575$EB3B77BB-460C-4C9E-A281-BEEAD5D1982C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f22790b7d685d2c32362b8971015fd7b35add539","datavalue":{"value":{"entity-type":"item","numeric-id":25009,"id":"Q25009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$BC4F6BDF-5D78-4E1B-A948-7D6DD0986224","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":"Q2961575$4A1183A6-3BC5-4B25-B1F9-724E415605BD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c8ce448e9ca90a1ed0697e1d55ba380fa4e809e5","datavalue":{"value":"https://doi.org/10.1007/978-3-319-52234-0_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q2961575$DE1D1D53-849E-4C93-9CDC-04635BD4C04C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"45b4d2b2ce3c71f0b7f0f2f6c1e1b48037685d7b","datavalue":{"value":"W2571168937","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2961575$35C22B6A-1B91-441C-A206-B42CD02BB6AA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"028b173fd504347e5ec217a7eca5bf3210ea8348","datavalue":{"value":{"entity-type":"item","numeric-id":3453240,"id":"Q3453240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$E9614580-6747-47C6-97FD-3D565617B457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$E9614457-EE6F-4300-BEAC-5F7053E7C956","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":"Q2961575$653FB511-B333-4E9C-9CA4-4A5228C1B130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69b0a1a9bb534c42ea053297bebfa6cf421e4b4a","datavalue":{"value":{"entity-type":"item","numeric-id":3612476,"id":"Q3612476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$7FCCE380-75B8-4559-B73A-D4062669C03B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a12c8e6968784fcf3cb8105db0edc338d9a5ec0c","datavalue":{"value":{"entity-type":"item","numeric-id":3192189,"id":"Q3192189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$A0DE5AF8-08F9-4928-A1DE-4BC0CE06E9A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4960d97c11c0cd0f282650fb582b7cd310577033","datavalue":{"value":{"entity-type":"item","numeric-id":3256638,"id":"Q3256638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$6A723E5B-17A8-4FC5-9F50-52E57B3D192A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3014ed8593967d1b0f8f5a23078b1e5b72049db5","datavalue":{"value":{"entity-type":"item","numeric-id":2786906,"id":"Q2786906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$D552F872-F0C1-4DFF-88C6-B9E3166B3B27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$7F1C2934-E730-4A81-9A08-C420586AA3F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37706997c0e12650bf30406d5f3ef502cc6c8e28","datavalue":{"value":{"entity-type":"item","numeric-id":2351157,"id":"Q2351157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$C42BFA2F-307F-4C6C-ACFB-DE5E41F1F996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f69516d40ec97b384f70501283c3b5c722beb3b0","datavalue":{"value":{"entity-type":"item","numeric-id":2830009,"id":"Q2830009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$7260CF66-B495-42DF-A824-D9628105DAB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40359969f4f5859125eed64808cf617ffbded116","datavalue":{"value":{"entity-type":"item","numeric-id":3992465,"id":"Q3992465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$9EE941EA-4FA5-45E4-AA10-659275AAC606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99b4eae7493d8f6c982d7549031f59a2b3902483","datavalue":{"value":{"entity-type":"item","numeric-id":3922169,"id":"Q3922169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$0E5FBA2E-2B11-4C15-A5E7-C6E008951A6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febe5bf101c3b7d6dce19439eb466caa5715de79","datavalue":{"value":{"entity-type":"item","numeric-id":5624683,"id":"Q5624683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$703EBCB6-787B-4B20-A2E6-8221F9D8EDE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8be9375a315209f41df1b38374a5e7e956d28bf","datavalue":{"value":{"entity-type":"item","numeric-id":5807665,"id":"Q5807665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$CA33B490-F8BF-4A3E-867F-F48338517A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"add4491e8fd66ac82b780ec4494c2c2d28510122","datavalue":{"value":{"entity-type":"item","numeric-id":677553,"id":"Q677553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2961575$C4896A15-512F-4249-92AF-09953264A844","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7de94fdb67b3ec18a4a9afac48a95b409770048b","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"68c94bf268a2c4a89af43a04704087c40b789862","datavalue":{"value":{"amount":"+0.845422625541687","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":"Q2961575$21894BC7-7827-468E-AF6D-D48EB1D17B77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"98bb4753ac749e013be85f4de658b00a7bdea261","datavalue":{"value":{"entity-type":"item","numeric-id":1656597,"id":"Q1656597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e56e0f454929b3298c98890964cc8ea834ce7668","datavalue":{"value":{"amount":"+0.8078352212905884","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":"Q2961575$768A6C9F-E436-475B-A0E0-B24ADD5431D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"29b2ac445d0887cb0feed7d7f9bcee96115a3e34","datavalue":{"value":{"entity-type":"item","numeric-id":2830009,"id":"Q2830009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28f7198ddb7986b412d6371e09c87376254ab232","datavalue":{"value":{"amount":"+0.7977145910263062","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":"Q2961575$F13300EC-1811-45EE-B86C-09AFD2476C5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97d68bcb8084a36ed362b6555c581cc66937378b","datavalue":{"value":{"entity-type":"item","numeric-id":4972164,"id":"Q4972164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"750425a93dab29170537c7ad9af71a7aa5de8f3b","datavalue":{"value":{"amount":"+0.791160523891449","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":"Q2961575$7981F372-3289-4288-B167-4D54165CDC82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"afe6d7bb0674a6cdba5cf502ac70a32860d40de5","datavalue":{"value":{"entity-type":"item","numeric-id":832268,"id":"Q832268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0f92466fe769dcbe3b08cebb21a7e2676a52548","datavalue":{"value":{"amount":"+0.784241795539856","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":"Q2961575$9C5035D5-989A-4E4C-A78D-CCBC8E050686","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2961575","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2961575"}}}}}