{"entities":{"Q3455223":{"pageid":5234623,"ns":120,"title":"Item:Q3455223","lastrevid":52407215,"modified":"2026-01-22T14:09:43Z","type":"item","id":"Q3455223","labels":{"en":{"language":"en","value":"Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \\(\\operatorname{DPLL}(T)\\)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6516105"}},"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":"Q3455223$91002BB1-4093-4397-8C71-BC93A749689B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9971e168f1e095d8a01a8d0e3e06e0142ee7af88","datavalue":{"value":{"text":"Solving SAT and SAT Modulo Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3455223$A50F93F0-5C3D-4F73-A2EB-3D3BB37DD7E0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8c20ef9d05c24ebea6b5fa6115277aac77593c23","datavalue":{"value":"1326.68164","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$49AADF78-C4CB-4B56-833A-B133F2B88E0C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"61c89a65d77f192eaebf63c149b98df5a3186264","datavalue":{"value":"10.1145/1217856.1217859","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$44138B2B-949D-4F01-8088-A192D501A87A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1e6a58ff964b9ca97414f0c42659717fa8e6fc43","datavalue":{"value":{"entity-type":"item","numeric-id":475169,"id":"Q475169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3455223$BD3028CE-A454-47DC-A969-0A591848E67C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cfd1da8b09a3144b32ef026d1d9b2bca68560b37","datavalue":{"value":{"entity-type":"item","numeric-id":438574,"id":"Q438574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3455223$9B0166A4-52A1-48B5-B302-4B39181E97B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3455223$8E907C35-0F29-4C67-97F5-14BB3674393C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f12bfc80fe4a431c556e028f5134a217234a7cc4","datavalue":{"value":{"entity-type":"item","numeric-id":63915,"id":"Q63915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3455223$C2DF04D7-9BAD-463A-9063-EB7D0B4A5616","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a7d3284117870528c81a7d62ae9b72c6a4498f44","datavalue":{"value":{"time":"+2015-12-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":"Q3455223$6D115C3C-6ACB-493B-AA2A-783E5527A9A3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$88C34206-BB40-4CD4-BB7F-C7D1CD8BDDD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$F3942C5C-988E-4052-8741-05AF40252B2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$D9275C87-39E8-4FD1-B6BD-08FA189DEE03","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"797de478e1afc99a91ea5e73b9428aaf713cdc79","datavalue":{"value":"6516105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$39B58AA6-9E0D-4E1B-A665-751D03DEA381","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543c7d0ffd0c52aa92a423848e3694a5bcbfca1e","datavalue":{"value":"SAT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q3455223$DFE81CA6-8888-4147-AF2B-E19FA2CC0232","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q3455223$6136E1F2-35F3-4AC9-9300-FD5E2EB988E2","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":"Q3455223$7BC00A37-8618-470A-88B1-D621F171A7A4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cae6a42e2b81289bab4dc74b5d2ab8cf6fa5dbf1","datavalue":{"value":"https://doi.org/10.1145/1217856.1217859","type":"string"},"datatype":"url"},"type":"statement","id":"Q3455223$1C603370-5AE5-4E00-9AD9-E095765E6188","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"16da3d4a468b131a4c168f7c4eb0eda4409657cf","datavalue":{"value":"W2022846948","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3455223$90D70886-3D22-4EFA-A2AC-8C79304E10F5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad4a777bf0bb99053f551e2b6fa0361d1c8156bb","datavalue":{"value":{"entity-type":"item","numeric-id":5705940,"id":"Q5705940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3840499de56922429c78cd783131ccf1f367a22","datavalue":{"value":{"amount":"+0.911723256111145","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":"Q3455223$FDA52168-4B06-4CAC-8B8A-ACD1A6A4B927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b4f0140fe152f7d5b3dfb3ede13e3c31df060015","datavalue":{"value":{"entity-type":"item","numeric-id":2926657,"id":"Q2926657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"547649e1151fb3ce7eca48f4df28708a8caac519","datavalue":{"value":{"amount":"+0.8572476506233215","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":"Q3455223$C00413EE-AD75-4124-ACC4-3FC31CBB9222","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f73ef4e4cd40d6dc34268d177258481051eb4b8e","datavalue":{"value":{"entity-type":"item","numeric-id":5716574,"id":"Q5716574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8682123f72dc4f80edbf5b78c49854b31495b51a","datavalue":{"value":{"amount":"+0.8503814339637756","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":"Q3455223$72399F19-DB2C-4FD5-9B40-6C51F34FE738","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47227c3ededf306d0bae5b081c3c2eaf0e20bdbf","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"589c098bcef5e5072e8398de7c2968281cdaa6cd","datavalue":{"value":{"amount":"+0.8493307828903198","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":"Q3455223$87F04D50-B7F1-4D13-9F54-B7864517A17C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060b299a48c3179c59c6541e6cf5829c59574c76","datavalue":{"value":{"entity-type":"item","numeric-id":5434475,"id":"Q5434475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d0d282232e215377c67724554fad3e75b6d314c","datavalue":{"value":{"amount":"+0.8429409861564636","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":"Q3455223$95B15CA0-427D-4B11-9057-E4E6C58B91E8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3455223","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3455223"}}}}}