{"entities":{"Q5191109":{"pageid":7220681,"ns":120,"title":"Item:Q5191109","lastrevid":50728727,"modified":"2026-01-14T23:14:05Z","type":"item","id":"Q5191109","labels":{"en":{"language":"en","value":"Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5587946"}},"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":"Q5191109$E9BC413F-761E-44B1-82E9-1B6052993C5F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e035e06ee00201f5322348da5d38e30f0dc3531c","datavalue":{"value":{"text":"Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5191109$4EB541FF-9E38-4B2B-88E9-1375509E949A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"792270ae2bd16b1c5060063078ee6af6820625d2","datavalue":{"value":"1250.68184","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$61A12EE5-BC00-4EC4-9129-CBCD6821DD69","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c02897c94d09150a3201e0f75307ec87a4bcffa9","datavalue":{"value":"10.1007/978-3-642-02959-2_23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$D3C44448-5C76-419D-BA8D-5042CE7DFC0E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f18c2b247eb825a22ef1ac6c7e11ce559c2677f","datavalue":{"value":{"entity-type":"item","numeric-id":438573,"id":"Q438573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$5E1078C9-5051-4C53-890E-F25D16C3B5E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"30c863fa396706b2f00b0e4efd36ab68137f900a","datavalue":{"value":{"entity-type":"item","numeric-id":293292,"id":"Q293292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$D69F7297-3B3F-48B9-ADE0-D9F2FBD9FBAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9a1766d1bc37a94f1b3bc2e2577c39b702d3f3e","datavalue":{"value":{"entity-type":"item","numeric-id":2871850,"id":"Q2871850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$7EBA4639-3458-47EB-86E9-B8438FB5C6D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f1c6f3313098f94ac950042b92865f2f95306b33","datavalue":{"value":{"entity-type":"item","numeric-id":438575,"id":"Q438575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$EBDF73C6-FD46-444E-A735-7D5ACD602E3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"076f42ceb107ac95ece0987fd254ab37feda8487","datavalue":{"value":{"entity-type":"item","numeric-id":352976,"id":"Q352976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$84CF2B87-35B2-4C1A-89B9-06F688BA0B4F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"cc7799424afce15eb24475c2c343f54bb5498c25","datavalue":{"value":{"entity-type":"item","numeric-id":5191093,"id":"Q5191093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$CE341FAF-F2C5-4B57-A045-DB10854EC6AC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"05720f4fd46426bc3a53a0e61b7abc572638b1a6","datavalue":{"value":{"time":"+2009-07-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5191109$C713DBCF-FF9F-440A-8E4E-98B30113E87E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"26cb7b1f9d57ab4a94e19bf2a042eb5abf25f8ac","datavalue":{"value":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.491.5880","type":"string"},"datatype":"url"},"type":"statement","id":"Q5191109$E1CB9913-CF93-4F90-BB41-85C0F783A5D7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$3D60BC37-547D-4774-B4C2-8945E7988F82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$E91FC278-F4CF-469E-958C-7AE46769D919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$A724D939-E36A-479E-8923-256C0D12E2AB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ec673f015447725a5d747cde238fb146784cc54a","datavalue":{"value":"5587946","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$1A3F6351-3543-4087-98FA-E8E67F8E0D79","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2440c6394e2ac24533843222855bcea18333dee","datavalue":{"value":"constraint solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5191109$E09DD9BB-ACAC-4718-9AAC-6051CF55D0F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"668c4fe6a3fc4e643381a2c84f3a6474c406ebfa","datavalue":{"value":"polynomial constraints","type":"string"},"datatype":"string"},"type":"statement","id":"Q5191109$22E20147-0DB5-4B9F-A647-A7AC6C61749B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d88b6e0f4b0254a0b4282c0a9f688566a888d5fb","datavalue":{"value":"SAT modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q5191109$6DF1D884-2BA8-423F-8B8D-E8AE5FCBF972","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5191109$A257B6F0-6965-4882-9890-923CA2FC411D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f668560f85d7afd1fece97b175bc3414226fbb","datavalue":{"value":"program analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5191109$6349EE53-F997-40B1-96F4-7E574A572BD2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"184b17ed6ef8f72f90ef44ecb976296d445c28b6","datavalue":{"value":{"entity-type":"item","numeric-id":21947,"id":"Q21947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$6896FF29-4B25-4FBE-9A54-1E9490137D6B","rank":"normal"},{"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":"Q5191109$21A7BF00-19C0-4412-868A-A172A0858BA0","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":"Q5191109$9076A57D-84A3-4138-8D97-7CACF734DDD4","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":"Q5191109$9A4B3501-5356-4A78-AF92-348927377C65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0c26e6916e0b9de30d3647f7e9e3f53ff40f0334","datavalue":{"value":{"entity-type":"item","numeric-id":19846,"id":"Q19846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$C68C6E69-A116-4A5D-A513-CF8621A73BD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"572143c91783d0a6b0c85b511e358973b6a75091","datavalue":{"value":{"entity-type":"item","numeric-id":21990,"id":"Q21990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$7340AC87-9F43-4659-98A6-7CB08708416E","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":"Q5191109$3D95C379-8846-42AC-9670-3B4B9BAEFB0D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a5fdc06db145e0cccffb39366279ac594ce7eeee","datavalue":{"value":"W1582592616","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5191109$BD22B268-ECE2-4715-B5EB-3AC8C74CDDE7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee132c4e5792ab38a0ff46d3d93155b8fcbe98d8","datavalue":{"value":{"entity-type":"item","numeric-id":1978641,"id":"Q1978641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$D717EA67-49D0-47ED-9FAC-67E91FA43D27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95127141592e878799f1620a9e20ee4ed2d5aea0","datavalue":{"value":{"entity-type":"item","numeric-id":5906950,"id":"Q5906950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$D3FE0718-0751-46DB-9016-6B2D4E921861","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01cea6af4ac375cfff93398a6355c2fe5e1792d5","datavalue":{"value":{"entity-type":"item","numeric-id":851142,"id":"Q851142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$BC4060AA-404E-4E5E-97D7-963C65E09D27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"065a2d65834e8c8b57bdda41356587a32ad9b5c2","datavalue":{"value":{"entity-type":"item","numeric-id":5457277,"id":"Q5457277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$96DE5C24-CECE-42F3-8341-64954A6E677D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc4469e6646035129caba23b24c5ef3fc5ec70eb","datavalue":{"value":{"entity-type":"item","numeric-id":3522012,"id":"Q3522012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$94E82F56-26D5-4940-9EFE-D0A43FA6F41B","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":"Q5191109$970F056B-B763-4CBE-A90F-4049CC2A66E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"233b9f4475cdb26cfc8da5745612d758a0f40a05","datavalue":{"value":{"entity-type":"item","numeric-id":5505493,"id":"Q5505493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$D0FD172A-09A7-4780-8A08-DF326738275B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb860ace0e36c82a8ecef7053057816d881aacc0","datavalue":{"value":{"entity-type":"item","numeric-id":3512493,"id":"Q3512493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$4B424FD3-C5FA-433B-974D-223289C6753C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9c3d7dfc55facbac01d8f787937a9b2b168b3e7","datavalue":{"value":{"entity-type":"item","numeric-id":5464701,"id":"Q5464701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$A4E3E731-BF4B-4741-9C8B-E0261F702396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"876f8e9697a35a1fa4e631a25500a97f4e320208","datavalue":{"value":{"entity-type":"item","numeric-id":876042,"id":"Q876042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$DAAD06F9-2A7F-4C3F-941A-621A9541C05F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c8e9433babfa01b39b72b0ddf6c5f892aa6f566","datavalue":{"value":{"entity-type":"item","numeric-id":5313720,"id":"Q5313720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$4242F646-574D-49D9-B9BE-8F2303219F69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6730550a11c6a1243c11c8b5e1cd605627b493d","datavalue":{"value":{"entity-type":"item","numeric-id":5475786,"id":"Q5475786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5191109$39199CEF-BCA7-430E-8478-7B62A591F324","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d38e6aaa02a6dd15149691d75689b8dee0520308","datavalue":{"value":{"entity-type":"item","numeric-id":438576,"id":"Q438576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5434388bd2f32825e061c35329204c977698e9e0","datavalue":{"value":{"amount":"+0.9197124242782592","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":"Q5191109$320500A2-6359-4E06-A921-D50D1F1B8EEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2bbfd54b1a8265b5163400539449c0671db6607","datavalue":{"value":{"entity-type":"item","numeric-id":2871851,"id":"Q2871851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8e10e24236ce2c5757865ab9e8b6cdc8a9b55de","datavalue":{"value":{"amount":"+0.8334420323371887","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":"Q5191109$618D51B0-59F1-423D-AB27-3FB1FCF2BD1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2ab284ca282458f5ee0350d83f2498c8c16f0df","datavalue":{"value":{"entity-type":"item","numeric-id":3612476,"id":"Q3612476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce6efc69d88bddbd40c76199a47bfc542c206fa8","datavalue":{"value":{"amount":"+0.8139145970344543","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":"Q5191109$5D680A53-D02C-40E5-9906-00E72E0D38F7","rank":"normal"},{"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":"35b883c32a9863b6eb1ebc0e0142a1017ea10cc7","datavalue":{"value":{"amount":"+0.7880679368972778","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":"Q5191109$871BAFF6-5350-4DDE-88A7-0FAA00951D85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5391bc9fd53f74aae20ee0a00abf3dc61ed6a51","datavalue":{"value":{"entity-type":"item","numeric-id":3066114,"id":"Q3066114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69d4364a444bf08f48f4d34a79777f3aa9fe300f","datavalue":{"value":{"amount":"+0.7880377769470215","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":"Q5191109$97BD0D34-AAA4-40B4-B923-E3AFE774634F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5191109","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5191109"}}}}}