{"entities":{"Q6957142":{"pageid":21246378,"ns":120,"title":"Item:Q6957142","lastrevid":84072536,"modified":"2026-05-09T09:38:44Z","type":"item","id":"Q6957142","labels":{"en":{"language":"en","value":"Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8065836"}},"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":"Q6957142$BE297639-881C-4A68-A824-D9DC75BCA244","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6ad2e470d15098e06a14f25216fbf586b91be7ab","datavalue":{"value":{"text":"Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6957142$57005BBB-31FB-4DC4-969A-06CDDD88062A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dd3eed34a322eea67f93a38a5c238c3ede4907f2","datavalue":{"value":"1569.68101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957142$2DB923D2-D57B-4380-945F-979BDF4FB81F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"86ef2900f9e902a9fdc44b1d7c13896030feee6e","datavalue":{"value":"10.1007/S10817-025-09725-W","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957142$B437D97D-125E-4490-88BC-5380D65B4C99","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d0c8330a4b879883ca5c73ff9597518a76159a54","datavalue":{"value":{"entity-type":"item","numeric-id":6535366,"id":"Q6535366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$492AE917-2403-47D6-AC11-7DD81D5DF754","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"027199b026f9abf199f45358e0a212ab76e02318","datavalue":{"value":{"entity-type":"item","numeric-id":2118344,"id":"Q2118344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$B02014D6-28B1-435C-9802-63185B45AC45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4545114e473836bad71ebea0181e527108d9e5ea","datavalue":{"value":{"entity-type":"item","numeric-id":352966,"id":"Q352966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$B2540DEB-402A-4CDC-9AB8-DCE226BCC09C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9afcc482ca2a503836b4b22d76e89c71dc77cae3","datavalue":{"value":{"entity-type":"item","numeric-id":6535364,"id":"Q6535364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$2BF5B796-F552-4CE0-9266-45B689BD7D4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"65191862b1e49d35d5ac78419fb25bec955bf14e","datavalue":{"value":{"entity-type":"item","numeric-id":1694025,"id":"Q1694025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$CE325A97-4FBA-4D3C-85EC-ECDDDF9A5C94","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":"Q6957142$25D38D0A-8B33-49D2-AEF9-8566DEAAD8CF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"efad754626f161cd66c554302db22bd9c4d46e2c","datavalue":{"value":{"time":"+2025-07-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6957142$7FE79424-BCAD-4C66-8D17-F0D1B8F5AFBD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957142$F7E2B31B-805F-49F2-9144-0D987D944062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957142$E3439A0E-C9A3-47A6-B14D-88FA7DBEF282","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"01c7a260d70a5a3674e7d7e87b03caf9e859b274","datavalue":{"value":"8065836","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6957142$1155E396-39DE-4F8C-ABCC-391F2C4A4C71","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$7E1293DF-E2CE-47B5-9DE0-5AFCDC52C938","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957142$188E71D1-B2D8-4940-8475-FFA315D404FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b36d924addd0d2f364b26835d91730b673a9f92","datavalue":{"value":"distributed computing","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957142$1BFA9251-21AA-4230-AB2B-442DAC21F312","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"44fac2abe78ae44f6c642045e37d45dc6bccca62","datavalue":{"value":"cloud computing","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957142$595FD3EB-8C9E-4F3D-B205-657130DEDA6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"079fd372b0e5e4842974e63d785072168d11e4fc","datavalue":{"value":"HPC","type":"string"},"datatype":"string"},"type":"statement","id":"Q6957142$A8C8B95F-5589-4F1A-94A3-B20AC6DA0FE5","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":"Q6957142$F058AFB5-C633-4480-AAB9-F42A70230D47","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"55abd3cb726d920bced8b1d2940097a0e68510b8","datavalue":{"value":{"entity-type":"item","numeric-id":3453220,"id":"Q3453220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$35ADD9E5-DF51-43E7-9767-96CF9B4EBE5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01d7d3ccc3684bd24073efc75ecbe050838f84f1","datavalue":{"value":{"entity-type":"item","numeric-id":5591930,"id":"Q5591930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$8B5AF7F9-90AA-45B2-A997-04B005184DE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65f86bfbb124f6a8581b22889d804be9da470078","datavalue":{"value":{"entity-type":"item","numeric-id":5918545,"id":"Q5918545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$10962A00-8DA6-4DB1-AAB5-9FF2AE4DCCE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cdf64b2a914be509f334d011c8426b5f7796a0d","datavalue":{"value":{"entity-type":"item","numeric-id":4930578,"id":"Q4930578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$142EFED3-156E-4F28-868A-E6ADEF33454A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9cdaa2ec8eceac1d3a0c164dd76be4ed6c68bc4d","datavalue":{"value":{"entity-type":"item","numeric-id":5946344,"id":"Q5946344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$4A6753F9-C012-4180-9FE4-72BECBB15FC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$9F35AFFF-B953-4EE9-BE9F-B525E130FC74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8dd91d0f75d460b40c4f5e874c6f021488cdb98e","datavalue":{"value":{"entity-type":"item","numeric-id":2060693,"id":"Q2060693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$C8683EA9-DB2A-4AE0-9577-8B1F48D52035","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$935190D6-6805-4571-B701-81C2FBE11568","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7822b32c270c4bed5a3c343d0bc07d27a793e5a","datavalue":{"value":{"entity-type":"item","numeric-id":3639756,"id":"Q3639756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$76E74842-4156-4433-9A9E-FAC9CCFA6052","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7012bf2c8e1ba10cf9896acdd463864da284937a","datavalue":{"value":{"entity-type":"item","numeric-id":2818017,"id":"Q2818017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$DE693EE9-139E-4251-8A06-62A969750296","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d43182de98d159f0ebb543c5126e0ae385036ba","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$C837BFEB-7ACC-4F68-A1C4-5C56F4AD7939","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7b70c41349e3cf065de8bfe6e202264aad6f5cf","datavalue":{"value":{"entity-type":"item","numeric-id":1394776,"id":"Q1394776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$F065E480-69B3-4B6C-9524-4368642DB8B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1951f16d4fe8a611f755a4887c35002e0149e28","datavalue":{"value":{"entity-type":"item","numeric-id":5919480,"id":"Q5919480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$4A5EE1AC-E0F1-44D6-929A-C9DC6573D56A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52cf18275213387cf215be837cf5c3464a4be860","datavalue":{"value":{"entity-type":"item","numeric-id":6535367,"id":"Q6535367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$AE3D94E2-E816-4A26-BD77-0ED752BCBFFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e8ecb2d6f36884d02916c2e1e3fb503d1c56f88","datavalue":{"value":{"entity-type":"item","numeric-id":3453235,"id":"Q3453235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$38FE5066-0DE5-46A8-BE6D-55206B0EBEBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cce922860f2a1126d5854cee853b0a72b2ecf9c3","datavalue":{"value":{"entity-type":"item","numeric-id":6643101,"id":"Q6643101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$86C7CFA1-79B6-4B31-89A2-432F0B687D5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88b8f502eefecfcdfdb968dfd0293dca3eaecf62","datavalue":{"value":{"entity-type":"item","numeric-id":5463402,"id":"Q5463402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$CE12CCDE-0740-4B63-A994-D62376A28DB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f9655213898b1b95cdf71db95e3bf0d93dc9d1e","datavalue":{"value":{"entity-type":"item","numeric-id":6487361,"id":"Q6487361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$21E56E3F-6366-4382-9497-2E6A104388F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1484285696f0e1a12d13ab196c38da736ba4c504","datavalue":{"value":{"entity-type":"item","numeric-id":6864414,"id":"Q6864414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$13F1138B-F6B9-4631-B23C-0385B4222549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ca64ffb3f397674160ee2f2d4b28cbfbd6479bd","datavalue":{"value":{"entity-type":"item","numeric-id":2118345,"id":"Q2118345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$F098067D-8EA1-49D1-838F-1C2AF75C874B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cfb8f8ba363369124e76cfe8ef214d8a77266fff","datavalue":{"value":{"entity-type":"item","numeric-id":6535369,"id":"Q6535369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$6DE9473A-77B8-4FA2-A2C0-0A84FBFF6171","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e99741ea86af8e3fe4690d90c224835231a7ef4d","datavalue":{"value":{"entity-type":"item","numeric-id":2233509,"id":"Q2233509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6957142$E4CD8218-E18E-4246-AFF3-9267E090B190","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Producing_proofs_of_unsatisfiability_with_distributed_clause-sharing_SAT_solvers"}}}}}