{"entities":{"Q5897077":{"pageid":7937688,"ns":120,"title":"Item:Q5897077","lastrevid":93306578,"modified":"2026-06-05T04:10:45Z","type":"item","id":"Q5897077","labels":{"en":{"language":"en","value":"Efficient distributed SAT and SAT-based distributed bounded model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5667316"}},"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":"Q5897077$76E7C85A-C259-4DB2-9AAF-F1E251AE23AA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b8c8f2d2ec76da52bc4ad5fba0da16b149a776d5","datavalue":{"value":{"text":"Correct Hardware Design and Verification Methods","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5897077$245A3A39-8252-4BEC-A584-DE7D54BE41DA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"072d4c436dbc3f438fd7c3d5301eddc09a4c776f","datavalue":{"value":"1179.68084","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897077$CCA446DE-2B3F-4B88-A1AF-F4367F6112A1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"267769ee025773c3257f441a0558f5f2a60f51b9","datavalue":{"value":{"entity-type":"item","numeric-id":432145,"id":"Q432145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897077$607BDBF2-735D-49B0-8DC6-FC7B10621D31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d28c0a406f6ee99cd8f5e212965690a891ace79f","datavalue":{"value":{"entity-type":"item","numeric-id":193842,"id":"Q193842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897077$6D78B4A2-1225-4907-ACF9-5466F9BAB688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aee8a4ecaa1abef1ca704f01bee315e6f78f7fa2","datavalue":{"value":{"entity-type":"item","numeric-id":685102,"id":"Q685102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897077$6D713022-08C4-4259-A3CC-239D72E517AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3495207d1965356b5c09ec509a7ee4275d91cd14","datavalue":{"value":{"entity-type":"item","numeric-id":947793,"id":"Q947793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897077$D211C6BD-23B2-48C7-9485-FA5F6A8C69E6","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":"Q5897077$559CD2EA-C99F-4307-A329-6B0A1192676A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"922e941384ccd68eb1997024165e5bf5ef775623","datavalue":{"value":{"time":"+2010-02-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5897077$7FA3531F-E5A2-4EE6-ADB5-C15D95A9979D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897077$893BFB92-D79E-4530-8C3C-949631353397","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3e69e0c3ecd1615a3837bff31b4e7f554ad6a3bd","datavalue":{"value":"5667316","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897077$BCBA58FB-C5B5-4C45-96C4-51F5D38C5E5C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5834864074172f90c0db592b61fbce75f9303a03","datavalue":{"value":{"entity-type":"item","numeric-id":16627,"id":"Q16627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897077$EE84648F-5117-4863-9713-7B0B672A0FC9","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":"Q5897077$708BD746-1FB7-4394-A3E9-E652FDE07237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1eaabc0e561dc484a85bd72ad458c9fb5f2683d3","datavalue":{"value":{"entity-type":"item","numeric-id":15174,"id":"Q15174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897077$11D6A940-057C-46CF-8874-6F0E4F181BCE","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":"Q5897077$ECB76E06-B479-43CC-9CFD-4F6CFB1A9280","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1b8c5cde1231ec6becb5c8cd63c3722e801c9211","datavalue":{"value":"https://doi.org/10.1007/b93958","type":"string"},"datatype":"url"},"type":"statement","id":"Q5897077$74A45AAC-EAEA-408F-ABE5-88549A94E31F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"652751e9bf248790b4e9b94adeaafb8d6cf26dda","datavalue":{"value":"W219731125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897077$CD06CDB9-6756-46F9-99D9-EE00ED327D99","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6fcbd4de8d7777e47679b10069f6a3080aceb1e6","datavalue":{"value":"10.1007/B93958","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897077$851FD108-3555-43E6-85CD-4466483F7B3A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f05d9027728050cdc19e8a7e0e796a7fb4268a71","datavalue":{"value":{"entity-type":"item","numeric-id":3069995,"id":"Q3069995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"380e5685b36c1e8a03e0c4a2601805679abb4298","datavalue":{"value":{"amount":"+0.7909729480743408","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":"Q5897077$69BC2182-FD07-4664-9AFB-03E182057478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6163a7aa78d81cf3b8065a62f631a6a5857595d0","datavalue":{"value":{"entity-type":"item","numeric-id":2754108,"id":"Q2754108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e92cafdb3f53ddf947f8bf223e1ed0985f30ff1","datavalue":{"value":{"amount":"+0.7843477725982666","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":"Q5897077$99705B55-F3DE-4796-A3C6-C7B4CFE164DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0337eec65669bdb027f080d3087ed0d70cc9320d","datavalue":{"value":{"entity-type":"item","numeric-id":4738483,"id":"Q4738483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"818062e8e954b61c9fa781ef1166cc58d695e3da","datavalue":{"value":{"amount":"+0.7775493860244751","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":"Q5897077$6C365CB9-D0B9-4464-8819-651C4C42936C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36efb17185f5ee397f5560683aa7220adac5335c","datavalue":{"value":{"entity-type":"item","numeric-id":2848663,"id":"Q2848663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a751ab50acca8f78b643342bb06ab88d41554093","datavalue":{"value":{"amount":"+0.770587146282196","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":"Q5897077$54FB9942-54A2-4D59-A41A-FC2A2F66A179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"417f3b972ebf403c2e595613f41ecaa318eb253e","datavalue":{"value":{"entity-type":"item","numeric-id":1878909,"id":"Q1878909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"740eeafe8e444f355899154f6a41280759272fe4","datavalue":{"value":{"amount":"+0.7678957581520081","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":"Q5897077$703339B7-9A3A-45D2-A0B7-7E28A5A16292","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient distributed SAT and SAT-based distributed bounded model checking","badges":[]}}}}}