{"entities":{"Q839035":{"pageid":840883,"ns":120,"title":"Item:Q839035","lastrevid":64724355,"modified":"2026-04-11T21:48:14Z","type":"item","id":"Q839035","labels":{"en":{"language":"en","value":"Formalization and implementation of modern SAT solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5600748"}},"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":"Q839035$B6E9E7FC-694F-4F85-89ED-FD349DCAAFCD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"83d0ab3e5312b68bccd38b7435da07bfd6a7a3eb","datavalue":{"value":{"text":"Formalization and implementation of modern SAT solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q839035$F8440B1E-3208-4098-BD6A-6F904C1CE887","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae089bb17adb0eb1c97e40ca1b263c3bb3bb821b","datavalue":{"value":"1187.68557","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$31F5722E-4435-42F7-A64E-FDCD482644B4","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":"Q839035$DF8E252B-96DC-47B0-8477-F6DF77E8714A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$0271AA1D-0DD8-448A-B6AD-47D778A1544B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cb4a7b11cbf8a3591d56dfc973401a20f55cc386","datavalue":{"value":{"time":"+2009-09-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q839035$D2879D8C-AEE8-4D00-B63F-D8C162C6F827","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$2A6A3B28-88B5-4230-A25A-3DC1F2692E68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$DAC924A8-B532-4127-9213-2A8EE0568A4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$79B39640-135F-4A1B-B291-7F608DACE6C7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"64efa27fc1d1ee49918fa989a471f981997a17ce","datavalue":{"value":"5600748","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$1D676764-8ECE-4D55-82AF-2B90A0420931","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q839035$8747ED8E-9E66-40F1-9B2C-8E3237205A76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f7ac674268224c9b1b4b60f07b959745a70f08d","datavalue":{"value":"DPLL","type":"string"},"datatype":"string"},"type":"statement","id":"Q839035$943EAAFC-1C28-41D9-BE08-10606B9FFADC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q839035$91FBC883-3652-4107-8B81-D43157A70FAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d607627523840bd0bf4407097f29a3a99ef4a0a8","datavalue":{"value":"algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q839035$7494E5B0-B991-4DE1-8694-B91875A9A6D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"43d8de44b3f88bd19a871628a3509981cd748562","datavalue":{"value":"data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q839035$3C69369F-305E-4753-91DD-8DD8FAF5AB47","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"60c977c73f66c80db6a0782a3e55d401ee00ddc1","datavalue":{"value":{"entity-type":"item","numeric-id":19150,"id":"Q19150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$11CDF838-4078-4C03-8326-7C3B9A47F99B","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":"Q839035$5DB56E9F-104B-4E4A-B3CD-94EB92D19EF8","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":"Q839035$2EEECE8C-9B46-4F58-B2C4-DA2098FC43C0","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":"Q839035$59D4C823-029A-4A66-8450-E7BC2ED3916D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"64bf9be9ab36c39dedc3bc5290b05b2b8e2c3646","datavalue":{"value":{"entity-type":"item","numeric-id":40545,"id":"Q40545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$E42E6EE9-4B00-4F83-82E0-E98B54C4A547","rank":"normal"},{"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":"Q839035$FC111ED2-3CF1-4CA7-A4DB-C42BCBE7DFCE","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":"Q839035$57BFB904-F0BF-4C53-AF8A-71C2435146E5","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":"Q839035$B6D5C7C5-4C61-45AD-9B7A-A9070579B96E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7e58dfcd56869e8e2934446544ab50adff6c9660","datavalue":{"value":"https://doi.org/10.1007/s10817-009-9127-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q839035$678DE265-E27C-4D3A-A9EF-70854637961B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6e6cbd1892ba59989c79e9e85ead57cf9b2e74bd","datavalue":{"value":"W2021196646","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$38B1F7E3-DE0C-492F-9438-0595D9E2680B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"652707f3c517fc0bc45fb7ef7e533228515c0c0d","datavalue":{"value":{"entity-type":"item","numeric-id":5715680,"id":"Q5715680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$9CB762D5-D077-45D1-A3F2-AAD9FE52728D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06abc869dee57fcd899da7ce0facfa1d28b4c229","datavalue":{"value":{"entity-type":"item","numeric-id":4473048,"id":"Q4473048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$55B4D3BB-C416-4E2E-B7DF-9858313FF074","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":"Q839035$F71B4041-18DB-4FF2-A1CD-C7FBDB71C84F","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":"Q839035$D40F8F8F-FC73-40F8-A3B7-20AD24427F8E","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":"Q839035$63F1EDF9-BC4C-4DFC-8F66-C0428E87A4AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$D6804437-3C7E-4ACF-BF7D-B170713C9C25","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":"Q839035$38C9E371-A26E-4426-8AF3-4F15EFC0EE8C","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":"Q839035$9B90FF94-22B7-47AB-9671-4C8982B92813","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e5fdc7a388e99bd2ab8aeeef9f0d0e53fac4618","datavalue":{"value":{"entity-type":"item","numeric-id":4413894,"id":"Q4413894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$197FE254-C99B-4567-925F-BDFA3420F420","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5e1604a00628ddd7abdcaadf06538f9adcc20d2","datavalue":{"value":{"entity-type":"item","numeric-id":4804883,"id":"Q4804883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839035$28BEF206-B1DD-40D4-8064-6D483A67DAA8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1c838b16207c3862bd867c216523865f6ace9dde","datavalue":{"value":"10.1007/S10817-009-9127-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839035$3AD3534C-48FC-40D8-A833-A71295D01991","rank":"normal"}],"P1643":[{"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":"7d0ccfc47acd7a819797546d88efc81a876695d5","datavalue":{"value":{"amount":"+0.8451888561248779","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":"Q839035$E8B96E6A-9EE0-4465-909C-2A717956B31A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94ddb4e80ed900f0a6c3c900ae860d15e4b60990","datavalue":{"value":{"entity-type":"item","numeric-id":3224685,"id":"Q3224685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80e3e5b7717ccb5154242d1e53b15debb79f379e","datavalue":{"value":{"amount":"+0.8393617868423462","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":"Q839035$BC73E1EB-9182-4B50-8EF3-F84CBF148FA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"875fa20a403e3086793eeefa974c2d02108a4d71","datavalue":{"value":{"entity-type":"item","numeric-id":3396552,"id":"Q3396552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"711dfd6122425d2520890f150f4e4ba6afff2ee8","datavalue":{"value":{"amount":"+0.8241332769393921","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":"Q839035$CEEEDB03-6B32-45AD-A846-78560586CEF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ea49af491734bb1eae9415b843e3fb6e2b96365","datavalue":{"value":{"entity-type":"item","numeric-id":5504707,"id":"Q5504707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0a2fc8063d82f24b1984f3ff8cbcb87eae0e52d","datavalue":{"value":{"amount":"+0.8132449984550476","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":"Q839035$DEB8FA73-50B9-4713-98C5-CCC11D7049A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ad1ae46a13dbdff43b01ae1250f32f6cb7d67ad","datavalue":{"value":{"entity-type":"item","numeric-id":3562927,"id":"Q3562927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a57f6322ca061617a0ef4856b9f428165fba495a","datavalue":{"value":{"amount":"+0.8076391220092773","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":"Q839035$87209FF2-AC46-45F2-A4EC-8447890860F7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization and implementation of modern SAT solvers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_and_implementation_of_modern_SAT_solvers"}}}}}