{"entities":{"Q606999":{"pageid":608775,"ns":120,"title":"Item:Q606999","lastrevid":63045156,"modified":"2026-04-11T10:00:44Z","type":"item","id":"Q606999","labels":{"en":{"language":"en","value":"Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5817536"}},"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":"Q606999$3DEB0063-C3D4-4F79-8007-D7BD304BBF43","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3f1dc821f2237274c4853b4b8a19fd354876d2f9","datavalue":{"value":{"text":"Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q606999$355DB138-3E2A-446F-85FF-0DC0A270233B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"66efb8c483dcec0e7cbb34ccbefaf88bd90a060d","datavalue":{"value":"1208.68205","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q606999$E6DA2A14-6F9F-4C79-89E1-1296BC67D498","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"30659652a6bb6474380a07a770377c63fcc6c983","datavalue":{"value":{"entity-type":"item","numeric-id":606998,"id":"Q606998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$ABCD6342-A5CB-47D4-9E34-A81E13626B06","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$9787B1D5-A1A0-44BD-BCB3-75A5143E3D46","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b1a8b0b4410e75478f392738ec80b73d0645c344","datavalue":{"value":{"time":"+2010-11-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q606999$6D36AEF7-913F-4457-936D-BE8EC1D2F135","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q606999$9B60CBB4-24FB-4F25-A718-6D294DF0EC6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q606999$84D03F05-43A4-4BDB-B95F-8E7B377C91EB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cce4377ac2e3a00739b642d7cc1f7e66daac0a57","datavalue":{"value":"5817536","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q606999$C7BADDAE-3C8A-4804-99BB-2B3CD8B264AA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95beeb304cf96fc46ea459300ada38395ccb79e2","datavalue":{"value":"formal program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q606999$9CEA14FD-D0EC-4935-A49E-67361F769785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"508def3536da451aaa16ab7a21353869c1e5bdc9","datavalue":{"value":"SAT problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q606999$DB1F264D-6500-487E-A4F3-C40CA81CF1EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ebcdf1765afe1aa29d302e3c021519c61f81717","datavalue":{"value":"DPLL procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q606999$4C59437C-08A5-4D88-9116-A23BF1ECB558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q606999$5E85418A-2C91-43C4-8776-8D420154A6EF","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":"Q606999$11C9561E-F7CD-4519-9523-18F8CC219DDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$D6267C3F-727E-4B5D-B203-6CDE969EEADC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$DCC36C36-AD73-4D01-B0FA-D30A4DC45AD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$98D387C7-D195-48E7-A872-E1F14CAE139D","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":"Q606999$95F393AE-5FEF-42D5-9AFA-CF4473EC43BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$0279CE24-14CE-40C5-A1BE-0B651A8AD266","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":"Q606999$E5898192-3F76-4007-8FE7-2C6C9BA283B3","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":"Q606999$4CFB1DAA-4CD3-4E1D-9DF0-51A8D45D1A8D","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":"Q606999$BE33C28F-CC21-452A-972F-E007F64724A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a0d7e9c791eda9ba399e77e8e87cfd0627413df5","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2010.09.014","type":"string"},"datatype":"url"},"type":"statement","id":"Q606999$DC189B86-FFC1-463C-8FC3-6A76236FD40E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1cf5f2a0c3c136e35d43f9136209a306d50de1ed","datavalue":{"value":"W1991066194","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q606999$D342CDEE-A50E-45BB-A80E-B1FF6E5039D7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f814032017aa40390d4c6f26a550d62bb08ff374","datavalue":{"value":{"entity-type":"item","numeric-id":5503674,"id":"Q5503674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$332188AE-AC4F-4FFC-9949-DEBB2987B09E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$E91A4DE9-A5A5-4C5D-95F0-CA1081C0621F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7948d2ae997be513a92df2486b836c4e1eaa12","datavalue":{"value":{"entity-type":"item","numeric-id":5667480,"id":"Q5667480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$3F674F58-8EA4-4C4D-A9C7-CE98C6AA1221","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":"Q606999$E41DC2B7-2A04-48E9-8917-DF8F9585BA4C","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":"Q606999$279F9DC8-359B-4FBD-90F6-5AFA595EAD3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$8B09474C-2770-4FC7-9D6A-E7ADB8A86891","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4e6adf13c6408e6c2eebe9bb0eee05dbe30b987","datavalue":{"value":{"entity-type":"item","numeric-id":3524998,"id":"Q3524998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$C27914E9-2784-480B-B560-ABBBBB8F6AF9","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":"Q606999$BFD212DC-A10D-423C-8244-AE75E3C92E9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a617eb423cf926cf28e96790e7d7448b32237e77","datavalue":{"value":{"entity-type":"item","numeric-id":3562927,"id":"Q3562927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$AD5CDCCD-FE88-442C-AC52-22CE66EED895","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":"Q606999$E1C2DDF6-CB3E-4485-8476-57FD06E47717","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$34B2845F-3F31-4184-8F88-8A3A081A2E09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$E2D09483-B047-469A-853B-7B69582DD7DE","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":"Q606999$1AF41909-8E36-46F3-A228-B6C325A5DBBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f769fe6ef8dd71200eafe07970c69907f40fbcb","datavalue":{"value":{"entity-type":"item","numeric-id":5179007,"id":"Q5179007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q606999$7480BD6C-D816-4AD7-BBBE-E81DDEEE39F7","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":"Q606999$C5AF3428-475E-4D48-8D3C-D91F4D6E78D9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d8395e73b77d19e2a838935638540bf127c3b44e","datavalue":{"value":"10.1016/J.TCS.2010.09.014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q606999$B06DC152-BD4D-4B22-BDF0-AA6CE768D82A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c98e3a2fca2e53bc3e7652a7ccc8979e2c9b05e3","datavalue":{"value":{"entity-type":"item","numeric-id":839035,"id":"Q839035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"496dd74a11bf1fa2017fa8a64f6fcf6a7fee988b","datavalue":{"value":{"amount":"+0.9081121","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$D5D3CC7E-89E7-4AD4-A87A-643C9D70B4D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea53f4d0daf48dd7127e69ca85211a01679fed0d","datavalue":{"value":{"entity-type":"item","numeric-id":2583288,"id":"Q2583288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0cdb252dcdc69fb790d672e5a0c9e2c9f3f88535","datavalue":{"value":{"amount":"+0.90467525","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$94AAF3A7-5091-4E6B-B33F-782D34942379","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12aaa4a36bdf05dc06c575e9e83887fbf42b685d","datavalue":{"value":{"entity-type":"item","numeric-id":1037401,"id":"Q1037401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff7f441feba791f19bfaca31289520e592b343c7","datavalue":{"value":{"amount":"+0.88670224","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$CD532808-7BD9-499B-9691-D0B99ECBAE56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9390b4ccc6dc9f08d9ed8cd2d7f1eed1c352e9ee","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff7f441feba791f19bfaca31289520e592b343c7","datavalue":{"value":{"amount":"+0.88670224","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$33317F36-31C5-4499-B5BC-47E4D8C9CB01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43030318cb195462e4d6ff5b5b5c56e675ac9845","datavalue":{"value":{"entity-type":"item","numeric-id":2180230,"id":"Q2180230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e01df54c6f913f77bba1b99cc01fad49eb505f4","datavalue":{"value":{"amount":"+0.88449377","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$C966A312-416C-4DEA-9E18-0D5104553B27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc6cf94a941e73c549de5f3f28639ca1516bdd9b","datavalue":{"value":{"entity-type":"item","numeric-id":5386252,"id":"Q5386252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b47b35055d1d664dcc1ae2d78a92e17a074519c","datavalue":{"value":{"amount":"+0.8815338","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$E5A03913-3688-4076-8A07-E362A10DACD9","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":"1295f9a089e6344df79850182ab0e2e73e553beb","datavalue":{"value":{"amount":"+0.8794143","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$610830BF-C5D6-4B58-A5BA-44AFBCB2C2AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"760a14bfabc4e10a8a1363a170fc2f2ca225ee11","datavalue":{"value":{"entity-type":"item","numeric-id":3079919,"id":"Q3079919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"757e51e17fcd257344ecc02f22d23564c0f2b2bc","datavalue":{"value":{"amount":"+0.87794733","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q606999$C29D3DF9-F966-4A66-A338-B1CD308CCB48","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_verification_of_a_modern_SAT_solver_by_shallow_embedding_into_Isabelle/HOL"}}}}}