{"entities":{"Q3069995":{"pageid":3080711,"ns":120,"title":"Item:Q3069995","lastrevid":51175424,"modified":"2026-01-17T02:12:53Z","type":"item","id":"Q3069995","labels":{"en":{"language":"en","value":"Parallel SAT solving in bounded model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5843595"}},"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":"Q3069995$8FE26DB6-A23C-42B4-B90B-70AF28C75CB7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"81590d01e21ee070921c14a0b244b87a8e812579","datavalue":{"value":{"text":"Parallel SAT Solving in Bounded Model Checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3069995$D111EE95-34FE-4F35-B19F-58208FE20AA7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5c8b15603f880f3ebd117fdb3b0b3e7a5ce7a89d","datavalue":{"value":"1213.68359","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3069995$8B30E65E-1042-4F8E-8118-25A6E0ECABB7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"03595cd73b96d5b235024b2e19a251d81caed080","datavalue":{"value":{"entity-type":"item","numeric-id":402123,"id":"Q402123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$CC07517B-F3DA-4BF5-B2B8-268E0F60D5DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"99cfc7b60e7d4aa9e2822bc8bbedca020651b4de","datavalue":{"value":{"entity-type":"item","numeric-id":453487,"id":"Q453487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$FD7B9C4B-9FAC-4CEF-A39A-CF3065AE38E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0db1c1d4758cc84ba91e5181bfa794ba378ebc68","datavalue":{"value":{"entity-type":"item","numeric-id":402124,"id":"Q402124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$A4D1860B-F97D-4083-B5A8-A0125AE241B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a014e6ba9fde789e090c1a340d6af73ab4b427b1","datavalue":{"value":{"entity-type":"item","numeric-id":394331,"id":"Q394331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$CE087A13-EF04-48D4-8837-066379EF9F49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b966f75c8c0aa46508c2e1a843d2d063ac4942b9","datavalue":{"value":{"entity-type":"item","numeric-id":883143,"id":"Q883143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$F2A06EC3-BB38-452A-B4BF-B48DCE2E1A2B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"90226e22c518bbf24899277aeaad1e3115bd0ee6","datavalue":{"value":{"time":"+2011-02-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3069995$A37B29E1-F491-43D2-BB4C-7EAC7C6EFFA1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3069995$2ECD8531-94A5-427C-B987-644EE9C7FF19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3069995$32000B0B-46BA-426C-B925-2ABF288FB1D4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"83512f9ec9f02d64493cbaa808a2b460f0800c10","datavalue":{"value":"5843595","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3069995$1D9ADE30-121D-44BF-93A3-36D86A61F30D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"855af08d63de68a214880a14dc080a2a72230738","datavalue":{"value":"parallel programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3069995$930EB5B0-BCD9-426E-A21D-94F2A1B66185","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3069995$EFD630D6-67F3-4513-B490-BAC5BA3545E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3069995$E1A6FE52-7BBC-45CA-A839-9629EC56BE11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a08efa1a08a750d06fca0196004a17a02a35c592","datavalue":{"value":"linear programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q3069995$854CDE3E-849D-4EA0-A249-12E3AA3977EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b03439e7dedf0c27568d228c7244768e0713fd5","datavalue":{"value":"hybrid systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q3069995$5032919A-340F-4ED6-9678-01184D01084C","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":"Q3069995$B67EE818-F736-4637-BE59-58B685329BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"799090580f36f14cb3f589f1081f986ae14b2901","datavalue":{"value":{"entity-type":"item","numeric-id":18260,"id":"Q18260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$48390456-5ADB-4A30-9C94-342E35767159","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":"Q3069995$43653975-D921-4210-BA94-D5B74B507C0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b029c35ffabe60b7d29584a6d40b4cb278ba542d","datavalue":{"value":{"entity-type":"item","numeric-id":18983,"id":"Q18983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$422DC620-425B-45F7-BCD7-71059D6A1410","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":"Q3069995$E0406730-0F17-4CCF-9243-11863029F243","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8297742f147adf2f83e4c13d3146049f9feb5e9e","datavalue":{"value":"https://doi.org/10.1093/logcom/exp002","type":"string"},"datatype":"url"},"type":"statement","id":"Q3069995$BBC2F555-FC72-4A11-8951-FD75BD9E4E34","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6cda38a4183bf823326403c0ba524fd5f3939650","datavalue":{"value":"W2041340053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3069995$9A02EC55-940D-452F-8FEF-B470BC43856D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b24c037a9f39110ab1b242cb0c86a1afaa3a3e52","datavalue":{"value":"10.1093/LOGCOM/EXP002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3069995$24BCB404-E8B1-4376-B3CF-2EEF2DFA206C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3069995$96691C17-D134-4819-B998-D980C21E60B3","rank":"normal"}],"P1643":[{"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":"985ba8d6a0a3f72ef6bf190472b1ca99e341f017","datavalue":{"value":{"amount":"+0.8176490068435669","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":"Q3069995$149261B0-0D89-4ED7-823E-18DCB93BBC05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97a1bf693cef9178aadd375963cd412c8809cc24","datavalue":{"value":{"entity-type":"item","numeric-id":3176368,"id":"Q3176368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94fe1144b23624ca10e147335b5a52e38b13543a","datavalue":{"value":{"amount":"+0.8076806664466858","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":"Q3069995$7DFB14E8-89FA-4819-9401-93119C009CF0","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":"33d4b478e13f2eaa26baab6fcf4b1a77813de33b","datavalue":{"value":{"amount":"+0.8043440580368042","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":"Q3069995$2BCA99DF-74B1-44FE-A27B-BAFB48A06FF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ad56d5cf5a0914eae3e1991359f1a1939c792e8","datavalue":{"value":{"entity-type":"item","numeric-id":5898914,"id":"Q5898914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"155435a613af50359c8fcec6726ff25d533a55b1","datavalue":{"value":{"amount":"+0.7999502420425415","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":"Q3069995$FA41AF1B-C5F2-4D80-9E0C-D6D60DDE34CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81a8ff0eed24031615660e07d37fbc5700ef480e","datavalue":{"value":{"entity-type":"item","numeric-id":6080505,"id":"Q6080505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2a16718d23cb9f352c0006d753073bb09437204","datavalue":{"value":{"amount":"+0.7935695648193359","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":"Q3069995$C7BED34A-00B6-4588-8BB6-699901A77A26","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3069995","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3069995"}}}}}