{"entities":{"Q5222981":{"pageid":7252551,"ns":120,"title":"Item:Q5222981","lastrevid":100586711,"modified":"2026-06-05T22:30:46Z","type":"item","id":"Q5222981","labels":{"en":{"language":"en","value":"A theory of satisfiability-preserving proofs in SAT solving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7076889"}},"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":"Q5222981$9B2F6852-0040-418E-B470-658D09B29E29","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8b7f363abb6f5aad77dc8da985c10d6705b34941","datavalue":{"value":{"text":"A Theory of Satisfiability-Preserving Proofs in SAT Solving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5222981$28627C17-27A3-4B78-9045-12C34E5200C1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"91b359657b304882bf8c01b820f0805c89a5407e","datavalue":{"value":"1415.68203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222981$55066C71-F17D-42AF-9418-043D722C03E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca432b2e16ad9e194c3af93cff128dfaded4c01e","datavalue":{"value":{"entity-type":"item","numeric-id":1799111,"id":"Q1799111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222981$95A09AB7-E594-45B5-88EA-B96BD733A875","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5493ce657ff2c3e3dc02ab18ea0d14e2e4a6291d","datavalue":{"value":{"entity-type":"item","numeric-id":748757,"id":"Q748757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222981$BD993467-E92E-4C67-B61E-1F8EB1C6174B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eae4601ff702bcaa610b94b3434abd8165930c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4645721,"id":"Q4645721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222981$F423A811-9172-410C-805D-DD9426629561","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"311afef0a4b95245df7f6c2908ad6e9d40f3f2be","datavalue":{"value":{"time":"+2019-07-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5222981$44B8151A-A512-4C65-A69E-63E9D722A933","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222981$0FA89C8F-5D52-4B27-8DFD-823ADE49B5A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222981$33DEC177-0CE6-49D2-8F05-724A7C50E679","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"01fa9b5fa77fcc13dc80bfe8045f01faf74e30db","datavalue":{"value":"7076889","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222981$64FC8046-F275-457E-8EB9-B8CD5BF9C106","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"90692354579df344f848e01b4d521c677c73345e","datavalue":{"value":"inprocessing techniques","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222981$2573F91F-E009-4B1D-82EA-07BCA3A02675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bdf2cfbc6e4ef9d6558d9f0ed6d4633eea496912","datavalue":{"value":"interference","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222981$6FBE251B-3DE5-4768-9283-95DCC5E3D720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222981$F3680D71-1BF2-4A90-8897-35557E2C49B5","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":"Q5222981$ADAF0D44-CFED-4099-9E66-CDC40CE669B4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c5de513617d8cce58052aa260eef13fcde0a4734","datavalue":{"value":"https://doi.org/10.29007/tc7q","type":"string"},"datatype":"url"},"type":"statement","id":"Q5222981$6F849165-35F1-4EAA-8752-80E2D8F82D4E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6ee735902bb447ed7a258cc988c07dd4310e28ba","datavalue":{"value":"W2907057313","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222981$503DA19D-1E42-4AF3-A28D-707A4F55F442","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f4e4773dea398f7f7650f23bf031441ab52d49ed","datavalue":{"value":"10.29007/TC7Q","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222981$DB8D192A-F698-44F8-9C3E-DE5D71E0C1DD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38ca69dbb2a24d3517677fc5d81e39fc165e7937","datavalue":{"value":{"entity-type":"item","numeric-id":2181921,"id":"Q2181921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a573cc56c1fc6606f9fab6004a57ab4b961959d4","datavalue":{"value":{"amount":"+0.7671088576316833","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":"Q5222981$1EEDA333-0D11-49FE-A0CD-0B81574DCCF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a26a7f4962a889a85653228dd045e79018e0222","datavalue":{"value":{"entity-type":"item","numeric-id":4645727,"id":"Q4645727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39fe5ffc5926972268879d63e33d8b9f79a8e540","datavalue":{"value":{"amount":"+0.7535325288772583","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":"Q5222981$89DE8CAA-7B47-4CBE-A7AF-8417BF37B8F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efb7d206d8f62fdc4d731460f7b5dd697a5fcb37","datavalue":{"value":{"entity-type":"item","numeric-id":2209554,"id":"Q2209554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0cea2dc92c2fbbd529082faf140bc56bb656f950","datavalue":{"value":{"amount":"+0.7492910623550415","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":"Q5222981$37B6A2D8-180F-410F-9A0C-9F7B5A996007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4fd319d3f3d0549dc990cb8bdf00c9505d81eda","datavalue":{"value":{"entity-type":"item","numeric-id":2835888,"id":"Q2835888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0c37beafbd681e0baa2a60d1a44ddab35e45509","datavalue":{"value":{"amount":"+0.7399856448173523","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":"Q5222981$D06483ED-34E9-44EB-A90B-9D00E2779022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c36d3312f2d09610a2170b7380e4e4dd1744e15","datavalue":{"value":{"entity-type":"item","numeric-id":2303251,"id":"Q2303251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"916d1f795c47c175b882eb22fd8215b387d73c48","datavalue":{"value":{"amount":"+0.7296320796012878","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":"Q5222981$0567E237-A332-42A6-A6CB-38B56911C023","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A theory of satisfiability-preserving proofs in SAT solving","badges":[]}}}}}