{"entities":{"Q3623009":{"pageid":5652915,"ns":120,"title":"Item:Q3623009","lastrevid":50643812,"modified":"2026-01-14T16:15:04Z","type":"item","id":"Q3623009","labels":{"en":{"language":"en","value":"Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5548985"}},"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":"Q3623009$54724F6D-2D97-4361-AB76-D7063B8A61F5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2c34a58dfc5acee39054bdf33d465aefd007a18a","datavalue":{"value":{"text":"Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3623009$F70FFF2E-0C37-4CF5-9535-33AF4EE07F32","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a23ff8ae29ff24ecf3f8446dd96b5faec8514815","datavalue":{"value":"1159.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$DA5801F3-BDCE-4D30-8B44-E8F1687B1302","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3d1567372100e87dfb36b28fca60c95c4474d173","datavalue":{"value":"10.2168/LMCS-4(4:13)2008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$EAB84E9B-0406-452D-AD68-CC4A01878C79","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e88be69c40b517dcf95562e728bf82dd0b4372ca","datavalue":{"value":{"entity-type":"item","numeric-id":372958,"id":"Q372958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3623009$9118296E-B598-46AA-9CDF-503609BECF26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7760d2294608b8a183e8edcaea7081a99d31bc21","datavalue":{"value":{"entity-type":"item","numeric-id":293308,"id":"Q293308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3623009$3E93E109-FDE8-4F30-8F6F-4EB34A3CFE92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"556b5f897f5d545f04c26b56d4624f5cc4b2661a","datavalue":{"value":{"entity-type":"item","numeric-id":195654,"id":"Q195654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3623009$182535E6-988D-48A3-8627-E83350177C65","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3623009$F290F7AA-72D1-44BB-8394-6912C13E1C5C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cc7396a377674bf1d1ad6a9c9bbfaef229fcbe16","datavalue":{"value":{"time":"+2009-04-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3623009$4F61AFF6-0ACA-49CD-9612-FEA59715BB0F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$079CDB59-3AF7-44DC-9663-72B7CF308257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$B006A31D-A4C0-4DDF-AD2D-DC116234A0C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$D8C8B7F5-582A-4C6C-9101-FCDB0124ADD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$52EE726C-5C97-4F9A-A821-CE8E3688B242","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fb8ff2d98c246d14eef577f41a2c8b0fd5a6e90d","datavalue":{"value":"5548985","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$D599E6F5-9187-4015-AF3E-A99AE9F996B5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"beacc345177607df4ab1f59f0170626c9d1a1d90","datavalue":{"value":"propositional proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q3623009$05862114-A173-491E-9165-48367FEA6DC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q3623009$D7809454-49F1-4AB3-B85E-5EA4B914284F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q3623009$DF0B9322-177B-4C4F-9AA7-1A4ADCE653A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3623009$2B574C4A-2697-46E0-880A-E1923BF0EACD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"612be38dc6332086efd6d593db6ed42740231e6f","datavalue":{"value":"weakening","type":"string"},"datatype":"string"},"type":"statement","id":"Q3623009$0E1DF05B-9D81-49FF-B4EC-646DC962A5E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50729adc5734b939c187fd45b0eb4d181e50361","datavalue":{"value":"proof search algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q3623009$ED9EC9E8-13AE-4FFC-863A-F98D06B827E2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"10ed1370106ab58118612ce8fef1abc06fcb61d2","datavalue":{"value":{"entity-type":"item","numeric-id":13776,"id":"Q13776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3623009$3B8606F3-0186-471E-9877-4339448C931E","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":"Q3623009$315BFF5D-11B3-48A4-B951-F872EC78E439","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":"Q3623009$8AEBEAC1-F4F7-463A-9D5A-BBE923AFE3E2","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"bf4bf6e5c54b142163c755debd0b784539ca5321","datavalue":{"value":"Q124817153","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$20F332F5-99DA-4370-8802-A2B7F089E480","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c63cdfba45c5fa7b7e1b3c5007a1245a1acff3f3","datavalue":{"value":"https://doi.org/10.2168/lmcs-4(4:13)2008","type":"string"},"datatype":"url"},"type":"statement","id":"Q3623009$06C8E354-44A0-452C-956D-EC71346AE06F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1d67b6b08a40b4040c82c0d06dc97fe66a73bb84","datavalue":{"value":"W3100513773","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3623009$DD0E8DEE-64C0-400F-A261-21CE2C8B09CF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"885912552c5b699189b6b014c8cd978b505b8ede","datavalue":{"value":{"entity-type":"item","numeric-id":5326452,"id":"Q5326452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"116e882c55cd5a792fdb8f3eeb18d5666d289bbf","datavalue":{"value":{"amount":"+0.8243096470832825","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":"Q3623009$C6816316-7A09-4591-B0E6-37799B0DF72D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e050f30d7185276802f36abdec5347610a74e3d","datavalue":{"value":{"entity-type":"item","numeric-id":5715680,"id":"Q5715680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e30007c94e0b3616368df87853623ac1cd685e6d","datavalue":{"value":{"amount":"+0.8089936971664429","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":"Q3623009$B0439310-43F3-4A02-8EC4-7D5E4D16F026","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00cb9494be1c0a53bbff2931f066e0b4a9c90b0d","datavalue":{"value":{"entity-type":"item","numeric-id":5415765,"id":"Q5415765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c87af764fa7e948030b6c6ffebdeb7fb58f6efa2","datavalue":{"value":{"amount":"+0.7899972200393677","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":"Q3623009$89E2F13F-E530-4053-B74C-941A40DE304C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e367b9365c51e5a796d1351242716e78cdb290d8","datavalue":{"value":{"entity-type":"item","numeric-id":5902141,"id":"Q5902141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d41e82570ec2ef8e86f49dbd485182847f152a86","datavalue":{"value":{"amount":"+0.7865208387374878","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":"Q3623009$CC64CE22-63F4-486F-AF81-8993C9706BA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"564012405708b6c6f09a5efd00b2e4ccd103b7dc","datavalue":{"value":{"entity-type":"item","numeric-id":5444704,"id":"Q5444704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"962348863c499c1929ee3d2add2f7ba17eac96a6","datavalue":{"value":{"amount":"+0.7858068346977234","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":"Q3623009$1D1E839F-363F-461B-B5CC-33CD52F866CC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3623009","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3623009"}}}}}