{"entities":{"Q430830":{"pageid":432597,"ns":120,"title":"Item:Q430830","lastrevid":61777728,"modified":"2026-04-11T01:35:24Z","type":"item","id":"Q430830","labels":{"en":{"language":"en","value":"Satisfiability, branch-width and Tseitin tautologies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6050357"}},"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":"Q430830$78BA6732-3C57-4298-B629-E6BD716CBC56","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fd0105fc01357a2ba0a14b84ccc5094cc4c83973","datavalue":{"value":{"text":"Satisfiability, branch-width and Tseitin tautologies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q430830$FE100732-2A80-450A-9087-6B86409DAD70","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"640938f8d63f58fa31f982c121620f93fe192050","datavalue":{"value":"1243.68182","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$C5F0BFC4-470E-4B33-82FE-E8BFED2E01E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dda6b61323c36da4336c78f2a00f81b412a8cdcd","datavalue":{"value":{"entity-type":"item","numeric-id":430822,"id":"Q430822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$193F771D-E7D8-4728-BCEE-CF619603A625","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c0bcfb4eb9a7ab6903b269f394ffde6834d9319","datavalue":{"value":{"entity-type":"item","numeric-id":1370854,"id":"Q1370854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$0598AEB9-08C8-4AA9-9B5B-6125889AB56C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4472b31ebff52fa964618256e5b76c8eb3e874c2","datavalue":{"value":{"entity-type":"item","numeric-id":172540,"id":"Q172540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$9DF32246-596F-464D-AD5A-783484A5E39A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f03a3c04b271440e0460d17b6cd1c270f9267efc","datavalue":{"value":{"time":"+2012-06-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q430830$B992BD3F-94B4-43A8-9C9A-9FD41C0A8C92","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$899AB492-FE7F-42D3-8520-F8928665C96E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$3E18E1E5-8B01-451E-8C55-4DB3594D7E14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$3C97200E-71D1-4BFC-BB58-F409518D9526","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$5145328A-A1D2-4323-89AF-41AC28DC779D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"693b20c9f2761057a7b6305664797716262aac5d","datavalue":{"value":"6050357","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$1936A6CC-777F-4F0E-834E-A7CB9381A250","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00bd6e1cf2bcfb675f5f59828684a40ea35e6261","datavalue":{"value":"SAT provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q430830$D107B9B1-5AED-4276-A01E-BFA0A0448AF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c503d1f307d11fe2dee746636a5b30bb12f8bf91","datavalue":{"value":"automatizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q430830$54674F10-5D74-443A-A104-459DA2F234E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"125f848e824041bf43e11dfb5f43ae5c6f8f7ef9","datavalue":{"value":"branch-width","type":"string"},"datatype":"string"},"type":"statement","id":"Q430830$6AD407A4-1728-42F1-A481-2E53D430950C","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":"Q430830$3DCB414F-5F54-4123-810F-46840CDCEB6F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"089f08106643f29a99bbda2b3bbddda3477e6f94","datavalue":{"value":"https://doi.org/10.1007/s00037-011-0033-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q430830$B0FDECDA-0299-48EC-B042-ABEAEBB5327E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9d3a38ce887ebbb4dd03b8aa1d37f16c216828a1","datavalue":{"value":"W3158535383","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$77957625-A187-455E-AA14-5D4DCD245ED9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"969f22c2e1fcc10b1a49b07f05e049c2339de4a6","datavalue":{"value":{"entity-type":"item","numeric-id":1884991,"id":"Q1884991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$45F3C801-DF72-4CDB-B992-E7806769D3A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50621bbf1c084d93515abb8fb9d0b9bcc1e49ecb","datavalue":{"value":{"entity-type":"item","numeric-id":4651526,"id":"Q4651526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$CFF909E3-7949-4616-A3C1-7244EC1DE0C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2dce6c4e91f261ac3ef4f20f30b6bcb71a22e70","datavalue":{"value":{"entity-type":"item","numeric-id":4681889,"id":"Q4681889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$74BF6D0C-EAF1-416A-818C-FFB23D1D33B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"088d50352df9ad001d77073382165c77d3798fad","datavalue":{"value":{"entity-type":"item","numeric-id":3395034,"id":"Q3395034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$F7D287CD-265C-4D53-8B5D-FEF31C038C70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2ca04c59b1468ff9eb03a30febcf55d98359908","datavalue":{"value":{"entity-type":"item","numeric-id":1094870,"id":"Q1094870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$C6FD5D41-920E-467B-890B-D736FD23E94F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0d45c01055f697d85430bbaa22270d0fdca6fde","datavalue":{"value":{"entity-type":"item","numeric-id":2741535,"id":"Q2741535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$C3BFB06D-1C3A-4408-8672-226229E966B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9074ee3d5efbd83e8d8f04ba3e757924dfd642e1","datavalue":{"value":{"entity-type":"item","numeric-id":1881219,"id":"Q1881219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$B7DC0664-8C9B-495D-B2E5-166BD98C8A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"224d4c80b882c8c65110953af69580a23e45bdd8","datavalue":{"value":{"entity-type":"item","numeric-id":1923563,"id":"Q1923563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$AAC7228A-ED94-4A08-BC50-A9535EE0C166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08b529296035947435eb136154e374f9657d895b","datavalue":{"value":{"entity-type":"item","numeric-id":4406287,"id":"Q4406287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$C23F603B-EA4C-4B91-A99F-7D8DF7BE26F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93084df5751505b3c6a721eac731896a3039b3fc","datavalue":{"value":{"entity-type":"item","numeric-id":4291429,"id":"Q4291429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$561C50D9-FF92-4237-96C5-931D9FC7773D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"770839834e9b2e75c5cac9d85b4f2bbde549b6c8","datavalue":{"value":{"entity-type":"item","numeric-id":4507332,"id":"Q4507332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$13F0F680-71BA-4176-A055-0DA1A669B22F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0361b2d4dbd6696a9452bae4ca788e7abdb86772","datavalue":{"value":{"entity-type":"item","numeric-id":5497123,"id":"Q5497123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$B5CE955F-8BDE-42D1-A2A2-613919FB9CD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"daf3e133365d57dfbd2c07919f3093669a42c66e","datavalue":{"value":{"entity-type":"item","numeric-id":5928867,"id":"Q5928867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$E3BE2001-DD0C-4448-9DC3-49F68ECC8889","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abc98b33e9a835a50512897138e07b56bd6f6bef","datavalue":{"value":{"entity-type":"item","numeric-id":3287337,"id":"Q3287337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$55015D36-7667-4224-8FDA-38539E79940A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8f0e3f7fd80f69ea95a1288c512c5cbf5c438c9","datavalue":{"value":{"entity-type":"item","numeric-id":4228486,"id":"Q4228486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$04320263-FF11-40C2-B9C5-2DF2DD1AE27D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4a8301ee2a4412c50f6ca3708d56cc316c8339c","datavalue":{"value":{"entity-type":"item","numeric-id":4010360,"id":"Q4010360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$8624ADCC-F762-4B9E-8477-2B4E9D314559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51ff8a807471958a38eef5720fd27b64677c1d24","datavalue":{"value":{"entity-type":"item","numeric-id":3869371,"id":"Q3869371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$7E019AC8-C20C-483A-87C1-758C024E1C38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a2a57b475ae76d5a53ffe9b99df300f7fdeea33","datavalue":{"value":{"entity-type":"item","numeric-id":3906439,"id":"Q3906439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$3F7B1BBA-6CC0-4318-9939-60A7C0888033","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0942c3ffeac8339c20eccc6667aba9b8af08cc5f","datavalue":{"value":{"entity-type":"item","numeric-id":3758729,"id":"Q3758729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$BC87E909-D836-4F8C-A5BF-1052F140B28F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e62926166610e171255ba7600cdacbb982331e7","datavalue":{"value":{"entity-type":"item","numeric-id":1179473,"id":"Q1179473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$3858EC44-1757-45EB-B9D8-B42B017F9F4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"398ef8bc27e00efd8312d46a33efaa0333728c17","datavalue":{"value":{"entity-type":"item","numeric-id":1892832,"id":"Q1892832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q430830$0CA6613E-F310-4A1C-8EE9-367BE7CE03F6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"228d19a8e18cb4174b3e889f73f67b6604e48e3b","datavalue":{"value":"10.1007/S00037-011-0033-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q430830$E6E87105-5AC3-44EA-988C-34284C7BD81D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"410116ad48c47fefe9b752df2eaf62a843a92da9","datavalue":{"value":{"entity-type":"item","numeric-id":5325859,"id":"Q5325859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5c6791931d28aac182961d39fbda3bd0d062669","datavalue":{"value":{"amount":"+0.8218290209770203","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":"Q430830$70D94F08-624D-45BC-80DE-808CF8F041E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8539d39031d0ec3daa5d1751229274c9c6523918","datavalue":{"value":{"entity-type":"item","numeric-id":4972153,"id":"Q4972153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f45524b6cfd7da96ba5748fa1280da0dbb3a0f95","datavalue":{"value":{"amount":"+0.7969501614570618","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":"Q430830$6BB52223-9A6A-4413-8A33-7B8FCCC068CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd8d5fd8a19bdb600c7bae7900dc553b695623dc","datavalue":{"value":{"entity-type":"item","numeric-id":2818011,"id":"Q2818011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1861606789c2d4452b806d71e00f6fb0adcdfc35","datavalue":{"value":{"amount":"+0.7869783639907837","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":"Q430830$16D8DD72-A69B-4BC1-9346-0EA22661E64B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2d29bbf1bbc9f5aba33489e7969f75d6c388d7e","datavalue":{"value":{"entity-type":"item","numeric-id":2894482,"id":"Q2894482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc676af29c427356901747fa247810bf1dfa877f","datavalue":{"value":{"amount":"+0.7869412899017334","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":"Q430830$618B2B93-15EE-475B-A27C-75DB311E4D56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"507b3bfe8aab15501c87e7358c5f5c7db473c6f4","datavalue":{"value":{"entity-type":"item","numeric-id":4406287,"id":"Q4406287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29a8bc8c6c211632ad9e85e8dda3d4ba077006cc","datavalue":{"value":{"amount":"+0.7808218598365784","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":"Q430830$565B97D5-0DE2-42B2-8A36-2AD05714E19C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Satisfiability, branch-width and Tseitin tautologies","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Satisfiability,_branch-width_and_Tseitin_tautologies"}}}}}