{"entities":{"Q5179007":{"pageid":7208579,"ns":120,"title":"Item:Q5179007","lastrevid":52227497,"modified":"2026-01-21T05:05:48Z","type":"item","id":"Q5179007","labels":{"en":{"language":"en","value":"The mechanical verification of a DPLL-based satisfiability solver"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6416653"}},"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":"Q5179007$E18A8C97-715F-4C12-8A7C-DA52D60C38B1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2fcd3f67354c94f4a5803d2f6b8231a1708eba41","datavalue":{"value":{"text":"The Mechanical Verification of a DPLL-Based Satisfiability Solver","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5179007$A9702920-18B3-40D2-94FB-08B3098BE178","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"615956dd855b029696ddbe38c61633e8d6b88272","datavalue":{"value":"1347.68307","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$1401AC54-13B0-4A4E-AA79-EF16BCAA7A4C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f977cc4afe30a7452131df7ff084411daffbbaa","datavalue":{"value":{"entity-type":"item","numeric-id":532428,"id":"Q532428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$1A5EA547-9571-4449-8F17-56A91B7546B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8851032f4f598ea2e804e082ac5816dc6e85b953","datavalue":{"value":{"entity-type":"item","numeric-id":5179006,"id":"Q5179006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$2246ACE4-8DF2-4721-A81D-D727F990F57C","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":"Q5179007$E21EC14E-026E-45DD-9FF2-3E256DCC7DF7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e3ae1d772ce191deb207c0bad17ca1d39804476a","datavalue":{"value":{"time":"+2015-03-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5179007$DAFCC934-43B2-4D13-82ED-410E6E875E60","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$A580D10C-7647-4134-A660-DBA91DA4DED5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$2F0262AE-CA6D-4438-87BD-5981EC3CE4B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$E0579FA2-7D86-4025-8DAB-5022A8798990","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7118e9408009f3b6862e5f1c6e0d096fae66304b","datavalue":{"value":"6416653","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$211B36F0-C32B-4FC3-AFAB-6F550C1BD7BE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"20ec78b25008456461de6c905d2d26525e47090c","datavalue":{"value":"SAT solver","type":"string"},"datatype":"string"},"type":"statement","id":"Q5179007$BEAC1195-9BFC-4B87-AB01-531EE1C2ED97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9f24b7228de8c0fcadbd4a1c8332d81927fb4405","datavalue":{"value":"backlumping","type":"string"},"datatype":"string"},"type":"statement","id":"Q5179007$A278FB0D-B117-4581-B904-3D90C5DD3650","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c95c76d9805d3acb5f7c1ae4000bdce77c00af30","datavalue":{"value":"predicate subtype","type":"string"},"datatype":"string"},"type":"statement","id":"Q5179007$F7D7233C-9B23-4D96-B3F7-3CA400844D48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9af64aff6f4b1584152e161c095f4457b67fd943","datavalue":{"value":"dependent type","type":"string"},"datatype":"string"},"type":"statement","id":"Q5179007$5343F037-4A19-4658-8B80-341EE60F68C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q5179007$93115A4C-48BF-4984-A2B9-01B0820C71F9","rank":"normal"}],"P1463":[{"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":"Q5179007$206E6A33-62AA-41B9-9A65-CE293B65B9E6","rank":"normal"},{"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":"Q5179007$797302F4-A78B-42A0-9C94-404CD57363A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$E118B64F-B567-4071-8E86-5DB78D68017F","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":"Q5179007$D1A13B95-8B80-40DD-8C11-CD483427E2D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$31698C85-10D9-45E8-B0E3-EFD42A34101C","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":"Q5179007$2441494C-FA3E-4F5C-945A-824A35E631CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fc3b651b7bbe695a67e48e86359a2e04cb5ed6c4","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2011.03.002","type":"string"},"datatype":"url"},"type":"statement","id":"Q5179007$D087021C-C9E6-4777-A84B-F80672265079","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"76e53e9be4ab7686982099ba7198b5a2b3a79021","datavalue":{"value":"W2080046595","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$74C3C3F9-871C-480B-8AEF-9F035B73C77C","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"741dec3057176e27308375e42d9c07e349a57627","datavalue":{"value":"Q113318278","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$72DF2814-0486-4E6B-853E-6DD19AA89F91","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$1DBA9438-BB52-4160-9485-295D83A222A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d759cbb44710c98e061bdcde73524e71230f37b","datavalue":{"value":{"entity-type":"item","numeric-id":3709921,"id":"Q3709921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$4E609EC5-BF31-4987-9F3E-74E83F2F1843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$A58CE4D4-FF0C-4A21-AE92-44F8F31CD017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$F00AC40D-9EDB-45BD-AB1B-763C7D735916","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b7764cdcf146e4a0366ed508de52f68bde7b0b2","datavalue":{"value":{"entity-type":"item","numeric-id":5429314,"id":"Q5429314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$19ADC45E-CB16-4414-A6E1-1F995FE633C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$3947812C-8B4C-4C5F-B54A-05A3D65013AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$74C9D85F-52CA-476E-9ACF-6DF68FC09174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea7fb806cb84b37335d37b3efe1590f8bc64cb5d","datavalue":{"value":{"entity-type":"item","numeric-id":839035,"id":"Q839035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$3598F279-379A-4143-8DED-59791BFCAFDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9269e64d2adca53bb2f298ca1a02b550d98c27a7","datavalue":{"value":{"entity-type":"item","numeric-id":4571400,"id":"Q4571400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$FD5E6D9B-A651-4D8E-80AD-0B1C1975191E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"caff94044d7e9e5c06d98ab72e868da5cf4fc6d1","datavalue":{"value":{"entity-type":"item","numeric-id":1821563,"id":"Q1821563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$9D7770FD-858D-47A4-B0FA-563CC493C8EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93870916f985296994d3e934a3bbc33cc4056cee","datavalue":{"value":{"entity-type":"item","numeric-id":3801105,"id":"Q3801105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$5E3BB7BF-A857-4C56-8ADB-BA196D8232A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f1a85252a4c0a5bb2b7a3eae3c76b6088496bd","datavalue":{"value":{"entity-type":"item","numeric-id":4296962,"id":"Q4296962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$8A230076-044F-4BEC-BCB1-6D2E1444BD4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a574e5aa189b3fc2747ed9f87d92c59b775e8e6b","datavalue":{"value":{"entity-type":"item","numeric-id":2722014,"id":"Q2722014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$E68C0271-650A-45E4-AA63-0C292207139C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"764c075c90cc5f529b627cfa105bd25d7bbcfdf7","datavalue":{"value":{"entity-type":"item","numeric-id":3682461,"id":"Q3682461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$94102D06-1726-4796-8A69-73BC9D3EFA0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7b5fa9b205a479f7043d1f02b59d43eb670dc95","datavalue":{"value":{"entity-type":"item","numeric-id":5234711,"id":"Q5234711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5179007$381606E8-273F-4220-B344-BBCED2B4621A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9bc86c2615f011e25cbb7550f599871f8586db19","datavalue":{"value":"10.1016/J.ENTCS.2011.03.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5179007$0CD39025-920A-4327-9087-F9E35B738C4B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32781204d1db0d50f0fed8e58f21ef2e924a069d","datavalue":{"value":{"entity-type":"item","numeric-id":5327347,"id":"Q5327347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2649d87fb017628d50074d1ace40e7deec873c82","datavalue":{"value":{"amount":"+0.8329946994781494","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":"Q5179007$93C15D23-4627-4CCA-BBD4-D458F05E419A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2be33ccab093ca2a6b6fd2b7057b69ca7524c000","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91d7b6ab7f52fa6ccc49b91dd563eb7e1cf46934","datavalue":{"value":{"amount":"+0.8181313276290894","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":"Q5179007$D1C997FD-BC0E-4E3A-9AA4-6BD603AC5C8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb0577f322474b5b3f242014ac9019394cc0c3e1","datavalue":{"value":{"amount":"+0.8126345872879028","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":"Q5179007$852F5458-C96B-4C08-86AB-588AB1EE17FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a107f55234536e2e675d2a36003e9039cb482f5d","datavalue":{"value":{"entity-type":"item","numeric-id":2891429,"id":"Q2891429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f172694ae0da7ba2e124024acebd98e7af8d3fe","datavalue":{"value":{"amount":"+0.8007180690765381","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":"Q5179007$10C9AA8B-CC0A-48EB-ABE0-0C474AE54487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbd1f875057910272dc1f6cefa7437b5d6cd54c8","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"679d93a87cefbbf07833033f3aa6d38871073a7c","datavalue":{"value":{"amount":"+0.79781574010849","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":"Q5179007$B47F3912-6087-40C9-8BCA-9879A4EFD5E3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5179007","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5179007"}}}}}