{"entities":{"Q6897667":{"pageid":20883337,"ns":120,"title":"Item:Q6897667","lastrevid":84183470,"modified":"2026-05-13T06:38:20Z","type":"item","id":"Q6897667","labels":{"en":{"language":"en","value":"The CDSAT method for satisfiability modulo theories and assignment: an exposition"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8123925"}},"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":"Q6897667$2719E15F-CD65-4235-8FA5-DE631FF6C377","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7cf0eab38348b1647c16ae60b898cb4753e430cd","datavalue":{"value":{"text":"The CDSAT method for satisfiability modulo theories and assignment: an exposition","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6897667$30D41B9E-849F-4FCC-B573-D0377893DCA9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2dd6654ccfc3d3d1cc05e5e533ad3ab587d92bde","datavalue":{"value":"10.1007/978-3-031-95908-0_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6897667$5E70B58D-42C5-42EE-BBBA-0B0B3093EAE5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$3EC41EE6-BFF4-4894-BA80-D42B54D33CE9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"804cb8321879b3a50f4d87280bc7c6e87039f39c","datavalue":{"value":{"time":"+2025-11-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6897667$2BB4C13B-91C2-4098-8E56-CC58B1DB7753","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6897667$1B393EE5-2F64-4C00-86B5-D27A13A70FAB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7140dacaea574a42a196ed337f44189c0fa686c2","datavalue":{"value":"8123925","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6897667$4C051759-5206-4DCB-A922-A2739B5FB668","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd0627e6c1fcb5fde09ed32d3475d7ab54724224","datavalue":{"value":"conflict-driven satisfiability procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q6897667$52EF4FDD-BAD2-4939-B89C-33C9006D60B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4fcd78e8da6c15f8925b69be50fc5549e2553534","datavalue":{"value":"satisfiability modulo theory and assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q6897667$4B2C20F7-8249-4248-BAF0-50B0B0A27A64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bfff88c2380e4c25bc3fa0710ad2e9544dd0740e","datavalue":{"value":"combination of theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q6897667$75189617-7E29-4A99-9413-531EB4F62839","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":"Q6897667$2CCAE9EF-DAAA-445B-9B6C-E3FFA95E88E0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"14bd97e9dec390545916db4e89e737371beca26b","datavalue":{"value":{"entity-type":"item","numeric-id":5387916,"id":"Q5387916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$33D93632-572D-40FB-94A9-EFD9D079A4B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10b89f95e856482d87c1eee104a58dbb5392af66","datavalue":{"value":{"entity-type":"item","numeric-id":2185458,"id":"Q2185458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$B25ABDD5-DE95-487F-9B58-045F905F4D3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d645e2b876ab109a4fadcb1ed7f0c554bc73185c","datavalue":{"value":{"entity-type":"item","numeric-id":2303254,"id":"Q2303254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$CC3F7355-33B8-4CDE-AE2A-5CC7B2F970C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3abb1020d45fa27ad50fa120d6a14f8aaf93020e","datavalue":{"value":{"entity-type":"item","numeric-id":832719,"id":"Q832719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$92A62700-B1DA-4B53-802A-AD38FCEBA7ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64edbd4b0368a46cc24983dcdc802e4982142495","datavalue":{"value":{"entity-type":"item","numeric-id":5310200,"id":"Q5310200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$7DB8EA7A-4107-4206-BC34-EE65B7A45BAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$B6A12F18-4BEC-404B-9A73-7B41C87CE46F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$A204E89A-BCBD-4CE5-935A-33F0FA64F62A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f64a9ce1df6d32a732886ec13ebc30e0107b2809","datavalue":{"value":{"entity-type":"item","numeric-id":2864402,"id":"Q2864402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$2793D79A-935E-4FAB-99DD-D85D8F493B95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$A2659DDF-287E-4AEB-B9B2-A9171140DD8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37706997c0e12650bf30406d5f3ef502cc6c8e28","datavalue":{"value":{"entity-type":"item","numeric-id":2351157,"id":"Q2351157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$0380A8BB-C6FA-471A-82E4-DED8D703668B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$6BAB9FE1-EB24-4094-AEDE-43DF25021DA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76f085e060cc02117b4ec73931c77617da801d17","datavalue":{"value":{"entity-type":"item","numeric-id":2473386,"id":"Q2473386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$A32DB158-3789-4EA9-80B7-C826A6EE3394","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4e6adf13c6408e6c2eebe9bb0eee05dbe30b987","datavalue":{"value":{"entity-type":"item","numeric-id":3524998,"id":"Q3524998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$4E8D6BA9-08A9-4658-880E-8F1831C3BFF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bbe72cc116925a801c6363ae53a473520b6daad","datavalue":{"value":{"entity-type":"item","numeric-id":688575,"id":"Q688575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$A13F92E7-FE7F-4C7C-A36D-C5CF294C828C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8eb10e99387b1ffe2ae259de73129015df5eec94","datavalue":{"value":{"entity-type":"item","numeric-id":3305326,"id":"Q3305326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$48676FD2-6CC1-4DA8-B01B-0ED271F0C1E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98b011ab831949ce741780553369025dd5b73c2d","datavalue":{"value":{"entity-type":"item","numeric-id":5148371,"id":"Q5148371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$994B1A0B-424A-4A60-9478-1F171429E600","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9269e64d2adca53bb2f298ca1a02b550d98c27a7","datavalue":{"value":{"entity-type":"item","numeric-id":4571400,"id":"Q4571400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$C8D75D77-3405-49B0-8E26-608786EFAA0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf127aacc48403a7b3907e5c9de96f1a874f90aa","datavalue":{"value":{"entity-type":"item","numeric-id":3636877,"id":"Q3636877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$5FFBF881-6547-4301-8CE5-426C74D25647","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$6D7A11DF-E74C-4ACC-9ED2-77C07F964D0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6897667$93AF4347-C40A-4198-89A8-AA46A2DC379A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The CDSAT method for satisfiability modulo theories and assignment: an exposition","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_CDSAT_method_for_satisfiability_modulo_theories_and_assignment:_an_exposition"}}}}}