{"entities":{"Q2633263":{"pageid":2644006,"ns":120,"title":"Item:Q2633263","lastrevid":56772186,"modified":"2026-03-23T13:32:30Z","type":"item","id":"Q2633263","labels":{"en":{"language":"en","value":"Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7052200"}},"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":"Q2633263$08342476-B588-42BA-B53E-DB1E411F277D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"779a56a718d2ec9e46121cb34f6f5639b24cedcd","datavalue":{"value":{"text":"Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2633263$0AE846B3-B721-4A76-99A7-528F9BC1A549","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b254e8e5d5540571a0f2ebb01ab6b0515558a47b","datavalue":{"value":"1461.68215","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$33A23DCD-2825-4F23-9326-3B0F03668FA0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$B521B829-E6DD-464F-8DA4-A0134F868DEA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"18e3aed7ec2baba1bc6b2c08988b16bb9ac0e77f","datavalue":{"value":{"entity-type":"item","numeric-id":82263,"id":"Q82263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$D4E92B1D-1F7C-4FB7-A98B-7F1183918D63","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8721ec9cf8de43034be561afa7e535bafe3c2e57","datavalue":{"value":{"time":"+2019-05-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2633263$8D9D805D-0B28-4CCD-8703-9CFEF9689C89","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d7b8696f74e0ac5123a1fcdd2d286f95642fe9a4","datavalue":{"value":"Summary: The satisfiability modulo theories (SMT) problem is to decide the satisfiability of a logical formula with respect to a given background theory. This work studies the counting version of SMT with respect to linear integer arithmetic (LIA), termed SMT(LIA). Specifically, the purpose of this paper is to count the number of solutions (volume) of a SMT(LIA) formula, which has many important applications and is computationally hard. To solve the counting problem, an approximate method that employs a recent Markov Chain Monte Carlo (MCMC) sampling strategy called ``flat histogram'' is proposed. Furthermore, two refinement strategies are proposed for the sampling process and result in two algorithms, MCMC-Flat\\(^{1/2}\\) and MCMC-Flat\\(^{1/t}\\), respectively. In MCMC-Flat\\(^{1/t}\\), a pseudo sampling strategy is introduced to evaluate the flatness of histograms. Experimental results show that our MCMC-Flat\\(^{1/t}\\) method can achieve good accuracy on both structured and random instances, and our MCMC-Flat\\(^{1/2}\\) is scalable for instances of convex bodies with up to 7 variables.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2633263$FF0B8799-EEB0-461D-BBA6-A8CA6C361386","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$46C9007E-0E22-4CD1-9725-275A03E0CC94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$14F43FB6-C483-49AF-812C-1FA11DB00964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e01671c873d801b913451010c0981a684c101d40","datavalue":{"value":"68W20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$4BA01D1A-8A60-40F7-8873-D36084C48248","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"21106a5b683e30a58ca6834258246a1cb7af3bed","datavalue":{"value":"7052200","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$AC8F4BDC-E823-4472-8196-4C430E51E052","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"57ddd6eccfd39765b59706385ccc0ef634cb67ec","datavalue":{"value":"Markov chain Monte-Carlo","type":"string"},"datatype":"string"},"type":"statement","id":"Q2633263$0EE34C05-FB6C-4CB4-884F-16DC500D402C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d88b6e0f4b0254a0b4282c0a9f688566a888d5fb","datavalue":{"value":"SAT modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2633263$354D16A5-3B5A-48B3-B256-37EC21F9DFF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7aed9c09744cda6e644dc8040b1c3594e52dd8b1","datavalue":{"value":"volume computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2633263$A4CF720B-DDEF-4DCB-8688-F857DD09A1F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6580bf5149e6aa0cd589a79d4be5444bdb1bfa89","datavalue":{"value":"flat histogram","type":"string"},"datatype":"string"},"type":"statement","id":"Q2633263$FE1D111E-FD18-4198-94AE-C227DCB2911A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"14003a50a44c20e712064b27ecfc39c8400dd7cd","datavalue":{"value":{"entity-type":"item","numeric-id":16824,"id":"Q16824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$96A1C5A7-9938-4DA2-9AA8-A76F91B0D6CA","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":"Q2633263$B5489213-04A9-4EE6-AD14-7949AFC31FE8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3a005d815d06a12092f0506cb30e908faa26534f","datavalue":{"value":"https://doi.org/10.3390/a11090142","type":"string"},"datatype":"url"},"type":"statement","id":"Q2633263$FA3167C9-3B1B-4E22-96CA-5F25B81D9D7B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"46f7b33d0cf2a388633001031fee8bdec4bb9460","datavalue":{"value":"W2890922211","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$5ACDC473-3541-430D-B075-7BEB4F715729","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"127c62f6e048e8ae433b3b5c8eb6d0901ef01e7c","datavalue":{"value":{"entity-type":"item","numeric-id":4302827,"id":"Q4302827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$4ED86055-03A4-4F98-B79E-8426403BA1B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98ff388f1854cc1183de8af7335052d365ad39ee","datavalue":{"value":{"entity-type":"item","numeric-id":3821581,"id":"Q3821581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$4C06A73F-BB3F-45D0-A859-313F381825A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b406f9b9ed254ac478a4a13f1c477e4396481d6d","datavalue":{"value":{"entity-type":"item","numeric-id":2248073,"id":"Q2248073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$0941E878-736B-452F-B627-05F437D6DDD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cba1d07dae14cc5134ffc3788a13ade150ee8b4a","datavalue":{"value":{"entity-type":"item","numeric-id":3460065,"id":"Q3460065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$D8E69747-8A07-4543-BA6C-77164396E0F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb6ca4c5980fb9f1902e1d77c54b8bccb32416ec","datavalue":{"value":{"entity-type":"item","numeric-id":1659994,"id":"Q1659994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$BB08012B-5507-476D-B4EF-F3425E7A852B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37cc666e9529d5c9986c275ba27fa5fd6a1da6c1","datavalue":{"value":{"entity-type":"item","numeric-id":963407,"id":"Q963407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$07CD7EEA-33FE-431B-BDF7-E43DB113E11A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e406d45ddc37598ff7a6dd419d5f52edb52f620c","datavalue":{"value":{"entity-type":"item","numeric-id":5191119,"id":"Q5191119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$B35D0C7F-ED8C-4F98-B7D0-2C40EA89CF91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c92aebe1288a33263b617b1b67a4323e7a616fa","datavalue":{"value":{"entity-type":"item","numeric-id":2643564,"id":"Q2643564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$2E27D5FD-BC66-4147-8B52-FDC1579E8A41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"469f7648c7d936cbffcff01f3f28aa5476d8200a","datavalue":{"value":{"entity-type":"item","numeric-id":2345986,"id":"Q2345986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$421E1773-5D46-4452-B203-42C826499BED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86efbf1cab594c5879a26468631099d7bca15a38","datavalue":{"value":{"entity-type":"item","numeric-id":2443184,"id":"Q2443184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2633263$812B3928-E443-4AFA-ABD9-D90DC777C62F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"db58967fbdcc7c2819801ac3fbb97e4f9f097009","datavalue":{"value":"10.3390/A11090142","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2633263$80B396DE-483C-4D3F-B448-EECB82183842","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a885fa6c1c18d0954b52e3d3ea8a81227069d72","datavalue":{"value":{"entity-type":"item","numeric-id":1659994,"id":"Q1659994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb74a9f4895eea0f2d81168fd5ce23091973fb00","datavalue":{"value":{"amount":"+0.8690032958984375","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":"Q2633263$21A65196-40D0-46DD-A301-D11EFD53360F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9fd3772806d2841fd15a7b3d34368f579fd6884a","datavalue":{"value":{"entity-type":"item","numeric-id":5191119,"id":"Q5191119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d9d128d1d021191fd8dc3bec61e08499e1a42d5","datavalue":{"value":{"amount":"+0.8019381761550903","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":"Q2633263$907EA127-69AF-4660-86D2-1D4862A6FC96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11b6a5486976c74e63954ea0bbb480ce32b05151","datavalue":{"value":{"entity-type":"item","numeric-id":2345986,"id":"Q2345986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f47fd84064394353236c0e92fa4392b6bf5ad62","datavalue":{"value":{"amount":"+0.8004441261291504","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":"Q2633263$5462935A-D420-4DD9-B99B-9DD597352623","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bcc0de09a2afea9a1626d45e744ea455012c8813","datavalue":{"value":{"entity-type":"item","numeric-id":5194954,"id":"Q5194954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30777e90e25d2f346224752baf3d25301584ed11","datavalue":{"value":{"amount":"+0.7726607918739319","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":"Q2633263$99E5E8E5-BEB5-4FA0-B273-B060AD29FB93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de1db8002b6915e68a9f0bc0f41875e6e57a8367","datavalue":{"value":{"entity-type":"item","numeric-id":1683928,"id":"Q1683928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46cd1e7308fc120881bdb576ccb7059e571ae743","datavalue":{"value":{"amount":"+0.769507884979248","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":"Q2633263$52B90153-A760-4DCF-8407-5EF4EEFFED6F","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":"Q2633263$FCC39558-0019-4859-8E15-A124F7500EEC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2633263","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2633263"}}}}}