{"entities":{"Q2051569":{"pageid":2062311,"ns":120,"title":"Item:Q2051569","lastrevid":78414746,"modified":"2026-05-06T11:32:21Z","type":"item","id":"Q2051569","labels":{"en":{"language":"en","value":"Optimization modulo the theories of signed bit-vectors and floating-point numbers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7433028"}},"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":"Q2051569$329D9362-AEB6-4561-809E-6FD51A45FCDC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d9095069b7109b9bf42062da12c5edc45c0771fd","datavalue":{"value":{"text":"Optimization modulo the theories of signed bit-vectors and floating-point numbers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2051569$303B0B30-7DAE-487D-B97D-96098CEC2579","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d815e8cf70ea3e857994d7efa2393de98d582fe8","datavalue":{"value":{"entity-type":"item","numeric-id":831942,"id":"Q831942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$8CF1B0DC-5AE2-4758-B2B3-185BAE8C56C3","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":"Q2051569$A7DD1D18-2FB2-4887-9F80-31F83E799F05","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$813E029F-93CA-4871-BB06-1E34CCEC08AA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5f514d788c7189561054f85987d5959a8ca7fefe","datavalue":{"value":{"time":"+2021-11-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2051569$7D35178C-8F5F-4480-B538-DC56640486F2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2051569$A1CCD745-47A3-4E2C-8950-28052043194B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"686fd46a5d62fda0b8391bd0a7c5425010cbf145","datavalue":{"value":"7433028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2051569$08B1D6E0-D18F-435A-903A-CF23A0BE3338","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7d343151ae44533b07c7808e4cdc209cfda3f8a7","datavalue":{"value":"optimization modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2051569$E767F13F-9C87-46C1-8D4B-5320E301E996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"076f8c7784fe03e9129b43dc8799b5acc75a6cb0","datavalue":{"value":"OMT satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2051569$3E1D3083-AC44-4668-992D-F11FE1F16393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3c5356d05486b2ae7558ae21da04c45e153a917","datavalue":{"value":"SMT floating-point arithmetic attractor dynamic attractor","type":"string"},"datatype":"string"},"type":"statement","id":"Q2051569$E16512F6-B645-4D1F-AA05-E92EA8CE0BB4","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1f27acff849365f4ab8e32d28fed6e6b1e1bc2ce","datavalue":{"value":{"entity-type":"item","numeric-id":20537,"id":"Q20537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$E27EEDC0-EA33-4B76-AA7C-3D8B14D7513A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e04aa926dc79457d313fa39599d20474b6244f84","datavalue":{"value":{"entity-type":"item","numeric-id":38020,"id":"Q38020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$0F55B25D-7C2D-46AF-B63D-4C31FAED5045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"81965717a4235b826eea77f69bfe50eb8647090e","datavalue":{"value":{"entity-type":"item","numeric-id":44019,"id":"Q44019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$9A0A886D-76A7-4B17-8412-C1B25325226F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"075bd4f0d0f46efa06d0219c176262a3c479185a","datavalue":{"value":{"entity-type":"item","numeric-id":12856,"id":"Q12856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$902C85D8-50C0-4D5C-BA16-292B8F5BA426","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"58e165eb815084f9a0c331d63332660ffc985e0f","datavalue":{"value":{"entity-type":"item","numeric-id":34457,"id":"Q34457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$5EF37D3E-BCDC-4582-BA50-72C9D0E14EB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f73b220ba5587942b20819a10a7828507204c03c","datavalue":{"value":{"entity-type":"item","numeric-id":46504,"id":"Q46504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$2CE7A0E8-7422-4E42-977B-703310EC28BE","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":"Q2051569$FBDB6A98-690D-463D-8B6D-608876E7DC69","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"08ecbd1e3ce8dc5db14e70577b58ef09f0e5f95c","datavalue":{"value":"https://doi.org/10.1007/s10817-021-09600-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q2051569$50FA716D-2A35-43D1-AF9A-55A21844E88C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fae5e61879c13fda6c4d3930918f5746c0240398","datavalue":{"value":"W3185622705","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2051569$1E4AF7E0-CE8B-42BB-BE06-C37A57034972","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbe4ab10d9aeeb94e50cb5d978b1533fcf3dbc9b","datavalue":{"value":{"entity-type":"item","numeric-id":2848685,"id":"Q2848685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$B5E741CD-C73C-43D9-92F5-4B5706054001","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33244f7bb6c04da758d56eac971580e07b647512","datavalue":{"value":{"entity-type":"item","numeric-id":479837,"id":"Q479837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$8377D556-FFBD-4F38-898A-5EA6E4EB51D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d4d5df30bde2099983c3bf5f07484cf1031c989","datavalue":{"value":{"entity-type":"item","numeric-id":3181652,"id":"Q3181652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$FE460CFD-EC06-444F-8EE9-480CDAB355EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d13c05844eeefea4da2bd8565e7b44a35d5777e","datavalue":{"value":{"entity-type":"item","numeric-id":3557072,"id":"Q3557072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$13C949F3-B5A4-44D5-B94D-0334D20AB7DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce0390e6c099065b6b613963fde558aa23fc43b0","datavalue":{"value":{"entity-type":"item","numeric-id":5326459,"id":"Q5326459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$C883CCBF-B946-47FF-9942-2470FE1D88B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb644c5841dd8ef7fdeb2c27817dada70761fc00","datavalue":{"value":{"entity-type":"item","numeric-id":5429343,"id":"Q5429343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$EC17322E-4ECE-4198-AAF6-0EADDC53927C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fde830d73447460bcd9989f9bfe0e707f2af8214","datavalue":{"value":{"entity-type":"item","numeric-id":3192080,"id":"Q3192080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$3658EC5C-559D-4816-B9AA-9DA451089248","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66abb9095dbc3a897723093a77a1e1d68df2b1cb","datavalue":{"value":{"entity-type":"item","numeric-id":5408453,"id":"Q5408453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$033DB065-5817-4F22-A252-DBEAB0B834E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5c060d6258d63ebf14a77434a67c0cf971997ce","datavalue":{"value":{"entity-type":"item","numeric-id":1688546,"id":"Q1688546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$CEBC00D4-B647-455B-97A8-DDD37D4D65E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"079d9a1453e37e4f063466335e73de85de7201e2","datavalue":{"value":{"entity-type":"item","numeric-id":5756563,"id":"Q5756563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$001EE78D-0548-4266-8729-853D347E2725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4cce0b297ea45b764421587f2adf2d11f4a3e78c","datavalue":{"value":{"entity-type":"item","numeric-id":2908520,"id":"Q2908520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$7370AB7D-30D6-4D63-8260-E3A824DE70F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"470998aa3ffb889685e1a96b368461dc00a63016","datavalue":{"value":{"entity-type":"item","numeric-id":2946768,"id":"Q2946768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$F18D872A-2CD8-4CB9-B28E-45EA52427827","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29ab79554c0ac8a4b417aad372ff9378ed98075c","datavalue":{"value":{"entity-type":"item","numeric-id":2303246,"id":"Q2303246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$4457C89C-DA5B-4174-AF6B-6FBC73385D2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2393cc1f4a69812cd1a5e250417a622bad35140f","datavalue":{"value":{"entity-type":"item","numeric-id":5194955,"id":"Q5194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$A8787EFE-8687-4B1D-ABA3-EE6D99EDD7CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eea76a1b537d6d689c859ac4072fa31762d97b47","datavalue":{"value":{"entity-type":"item","numeric-id":2305439,"id":"Q2305439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$C3E7448F-49B8-4263-964B-568490DD57D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cea4728999f2c2cfb259f0aa0245339515471e80","datavalue":{"value":{"entity-type":"item","numeric-id":1799086,"id":"Q1799086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$F74B5147-8895-41BB-8250-09B5C9F0C21D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c745dd663a2abd2b58056b348dbbccd23cdf6d8","datavalue":{"value":{"entity-type":"item","numeric-id":3192205,"id":"Q3192205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$E0C20EC4-4953-4DBE-88E4-021DDB2E5F0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"946c8fa23d04c4cd453bd93a38bbd56dd8043fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2362497,"id":"Q2362497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2051569$4095929F-B25A-437B-A0F9-0ACCCFB02CFE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f2df1174c7617926a01075b10fc71a96e839b81a","datavalue":{"value":"10.1007/S10817-021-09600-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2051569$64227BAA-21F6-45FE-87D1-907919B1F62D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"775ed25bbaec5f340894362c9b61f87db4966250","datavalue":{"value":{"entity-type":"item","numeric-id":2305439,"id":"Q2305439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd387ba4fab2b9ac8c7964314f8e764d23d8ba46","datavalue":{"value":{"amount":"+0.9653670191764832","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":"Q2051569$FF874963-D5FA-4A38-8ACE-90C9811C7B50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d44bc618097406b4f5d19921d1927b50deb3818f","datavalue":{"value":{"entity-type":"item","numeric-id":2303246,"id":"Q2303246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"840ec5fe029abb35aa91f97c4b82d0e3e11173e8","datavalue":{"value":{"amount":"+0.7883015275001526","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":"Q2051569$C362D2C2-3B9E-42F2-AF6D-BB90809EB3EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87f72eaf64504f2ccdb990ca833e860e59816256","datavalue":{"value":{"entity-type":"item","numeric-id":5194955,"id":"Q5194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2670db092c035448c9dd7362246ab77cee986b03","datavalue":{"value":{"amount":"+0.7658895254135132","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":"Q2051569$D92A50F6-7F02-4D36-AA1D-445A1474B41D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16839c25443af1f0ca407fedc6c659d44618ee57","datavalue":{"value":{"entity-type":"item","numeric-id":2946768,"id":"Q2946768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3ea3408cd790c0cf682b257f3d37674365f2df8","datavalue":{"value":{"amount":"+0.7176753878593445","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":"Q2051569$B033447A-FC77-411C-B83E-346915AD9273","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ff7971bb0d53dd6682991734c0c56234b675e6f7","datavalue":{"value":{"entity-type":"item","numeric-id":5408453,"id":"Q5408453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24674ad1ccf9ec1084cb8b8360e74b60494bb704","datavalue":{"value":{"amount":"+0.7172892689704895","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":"Q2051569$CC82B1D2-27A7-4944-A663-26D2B456A80E","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":"Q2051569$C4247CED-422A-479E-A143-6B91E976B45A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Optimization modulo the theories of signed bit-vectors and floating-point numbers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Optimization_modulo_the_theories_of_signed_bit-vectors_and_floating-point_numbers"}}}}}