{"entities":{"Q2864383":{"pageid":2875103,"ns":120,"title":"Item:Q2864383","lastrevid":51886610,"modified":"2026-01-20T11:42:35Z","type":"item","id":"Q2864383","labels":{"en":{"language":"en","value":"Compressing BMC encodings with QBF"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6236393"}},"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":"Q2864383$F8FD7EE5-F2F2-44D7-ABA7-802DA677E21C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"12b3c36008f3cf7933244d27c1f960e99ff4e96c","datavalue":{"value":"1277.68136","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864383$6A2DA23E-28B5-4372-827C-9A969AE5348D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"afbe2a40c65b7812f7238e1bb93138982186b954","datavalue":{"value":{"entity-type":"item","numeric-id":2845507,"id":"Q2845507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$064E68A3-C498-4DF0-AC86-CB38799F49A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"396db362b8f5a55e9aac7b42eacb07e40796d942","datavalue":{"value":{"entity-type":"item","numeric-id":209458,"id":"Q209458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$E65D6D63-8311-49D8-BFC6-3115135C031F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$D8F64204-C6CB-45F2-9627-3FB15E1676CF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"deb6cb3450bd256fc635dc32234471403070c2b7","datavalue":{"value":{"time":"+2013-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2864383$8D417CDD-D85E-47F4-B4DC-1A58A05A5137","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864383$AEE8F20C-FDBF-4C6C-8638-C87AD0410A25","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f864979feef2f0df08ed0ebc2b2bc423661b4ade","datavalue":{"value":"6236393","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864383$ABAAE2C5-CE40-4E8B-B9FB-E53F05A72F3E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864383$0261FD93-EAE8-40A7-9E47-8524168EF2DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"86858b19e06e7f53cefb9a2372bf5b13d0adff66","datavalue":{"value":"encoding","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864383$DECA7F8A-3AD6-4066-B013-CC22922D6468","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dc78b1e4558056e875de92cbf8329d0562afe86","datavalue":{"value":"QBF","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864383$23FAF214-F5DE-4E66-8DD6-DB48F126A634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864383$FC749E2E-39D6-476D-AD98-DD201B9DB152","rank":"normal"}],"P1463":[{"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":"Q2864383$42C6706C-F58A-411A-A84B-CDD9C94CC51C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efa7dfee3dd74aae04647605d0a9a987c7d566cf","datavalue":{"value":{"entity-type":"item","numeric-id":16316,"id":"Q16316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$6F98A478-5A0A-470F-B5F2-4F6991B652DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ca9a3b7221d86f39ba625c5cdafb4b84300080f1","datavalue":{"value":{"entity-type":"item","numeric-id":13515,"id":"Q13515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$1C84E326-5DE9-4B96-B9F7-D88D456E5D7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6ef83bc65a4e27e40a0f15cc6aef8f4086b5991a","datavalue":{"value":{"entity-type":"item","numeric-id":23327,"id":"Q23327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$F0B0E610-651F-4DD8-B538-64874977FF46","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":"Q2864383$A6D0CDEA-B5D1-40A4-B39B-4884806E4EF1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"dd80c9d3c671d49cf2df5d17f58afe53245d9e70","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.12.022","type":"string"},"datatype":"url"},"type":"statement","id":"Q2864383$0447CA27-E2E8-4939-94D2-55E93E409EDD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f8f99c8d553d360d01f4033d78ab9a27670c2e19","datavalue":{"value":"W2108530105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864383$B0F4C101-55D8-4CB0-9A5D-2FB914C1FC0D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"20bef91b5160a2ef823522f019afc62d44e0c885","datavalue":{"value":{"entity-type":"item","numeric-id":5493231,"id":"Q5493231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$3F2C1292-ED7F-4566-A0A4-2145F31134E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bda68c490d3eacdbb4c205fd2cca76126f0a9248","datavalue":{"value":{"entity-type":"item","numeric-id":5714773,"id":"Q5714773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$22EF0EC8-736A-4669-8C5D-55D7CB235618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5e59694ba693ed2b8af4b0c9c848f2b45a00bcf","datavalue":{"value":{"entity-type":"item","numeric-id":4817533,"id":"Q4817533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$DBD2832B-EA0D-42D0-AC3C-C3D14F4FBD97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f541623726371fa1e6609e8c2eef0b9f81a4c6c","datavalue":{"value":{"entity-type":"item","numeric-id":4804909,"id":"Q4804909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$A0F1F87A-9341-48B7-B40F-80948B14AD83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0870e13c4a5dd2b1ec6ccf0eb8fddafbaa000d2","datavalue":{"value":{"entity-type":"item","numeric-id":5713732,"id":"Q5713732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$546E1A4F-3920-410E-91A5-D01D70D9243E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e1a2bc812e5333b5582e9a89d0e222c5015c063","datavalue":{"value":{"entity-type":"item","numeric-id":4539620,"id":"Q4539620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$3EA7DD2C-331D-490B-83EC-6F072E68E69F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87957d20676b341fc2d415efa4c896e75ab57ba3","datavalue":{"value":{"entity-type":"item","numeric-id":4414397,"id":"Q4414397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$10F1B0DE-457E-402B-8AF7-6F258040EE47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8e9c7dfe2263cb88548446838aa8cb493a7f9e1","datavalue":{"value":{"entity-type":"item","numeric-id":5325879,"id":"Q5325879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$3FDA7191-9425-4135-AE57-E934E45BB528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e70afc75614113fd909ab00f77eb42be8071853","datavalue":{"value":{"entity-type":"item","numeric-id":3429159,"id":"Q3429159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$D9E8C548-5711-461B-8F59-B9137C3E849F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5fbfdc3423a13c0e159fffb7f2eefc9ae94ed175","datavalue":{"value":{"entity-type":"item","numeric-id":2996176,"id":"Q2996176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$B8ABBF6F-3D67-419E-AD66-EDBAB6C9B27B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"736a1d463d18d2f300e2b9600c3f86eae2986ef8","datavalue":{"value":{"entity-type":"item","numeric-id":2537313,"id":"Q2537313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$428F488D-D184-4EE9-82FB-29E869E2ACE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f33f843778dfabfeef453cdfa627d4b42c24908","datavalue":{"value":{"entity-type":"item","numeric-id":4131648,"id":"Q4131648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$1F131B1D-FE61-4023-B96D-BC7E5F872FFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1511d1df8e0084c6a3d84c674a4c8c727063cd1","datavalue":{"value":{"entity-type":"item","numeric-id":5714763,"id":"Q5714763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$44B9900C-E93D-406B-9AFC-652D8FF7188C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e98bea2faf0f1e7139247049b725eb54de257627","datavalue":{"value":{"entity-type":"item","numeric-id":5593816,"id":"Q5593816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864383$E7A1E162-6A09-45E9-9B38-320E79BD0D91","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"36e8ccb508381abb012711fb7316c05a2ecb76e7","datavalue":{"value":"10.1016/J.ENTCS.2006.12.022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864383$0C864716-0A7A-45EA-BC1A-F2ACAA9C3AA5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8b345d474a165642404f144f55c18150725e59ca","datavalue":{"value":{"text":"Compressing BMC encodings with QBF","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2864383$0C3623A6-8681-4A31-8DA7-E65C759EB35D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"381b5fbcd46a24011e59d90944023c6e905a64c2","datavalue":{"value":{"entity-type":"item","numeric-id":5713732,"id":"Q5713732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ddb9c1a4f864bf08868bbb95b1cc9515fe73f1c9","datavalue":{"value":{"amount":"+0.8405556678771973","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":"Q2864383$2F9BEB50-9361-4FA3-8F52-54D1990C7893","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2850ed93b9300f9fa6dfcd630fc70b3e6cd1a60a","datavalue":{"value":{"entity-type":"item","numeric-id":4735931,"id":"Q4735931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"615b6d8128adf989759ab6fdd91070176bc489fe","datavalue":{"value":{"amount":"+0.7802148461341858","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":"Q2864383$59587DA7-C83A-4C81-81CB-1929C79A724B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0abb94556291074b77f223ba7201ac1ac379b4b5","datavalue":{"value":{"entity-type":"item","numeric-id":3192192,"id":"Q3192192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0d58df39831f201e863a022f4a64d4688385a86","datavalue":{"value":{"amount":"+0.7732083797454834","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":"Q2864383$482BC34A-4098-4D6E-8C9B-6F1724687EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83cc427116e8e5de07b05e44314d4af2dec7739b","datavalue":{"value":{"entity-type":"item","numeric-id":5900311,"id":"Q5900311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fefeaa3acded4aca6607dbecee4f485f4a0c1a26","datavalue":{"value":{"amount":"+0.7722088098526001","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":"Q2864383$38FE2DB9-9861-4A14-8EC0-A6FCC3B2B757","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9662436ddba986dbfe8fb88fc949db265075c573","datavalue":{"value":{"entity-type":"item","numeric-id":3620436,"id":"Q3620436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f4fbb2e11afe9652fde53a29a445dcf294e8346","datavalue":{"value":{"amount":"+0.7687442898750305","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":"Q2864383$51DC4630-ED9D-41C5-A8DF-9C5F6591DC43","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2864383","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2864383"}}}}}