{"entities":{"Q6045007":{"pageid":13179163,"ns":120,"title":"Item:Q6045007","lastrevid":58653963,"modified":"2026-04-06T04:55:21Z","type":"item","id":"Q6045007","labels":{"en":{"language":"en","value":"What's hard about Boolean functional synthesis?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7689213"}},"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":"Q6045007$C5131EED-363D-4BA5-BF47-3717942221CD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2ade82803afc320f15634fdb2246dad2c44eb283","datavalue":{"value":{"text":"What's hard about Boolean functional synthesis?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6045007$4FB7499C-9A63-4C33-AA0E-F562803F0E8E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e3e0c3e3c6ab256684439599c52994c2f0499bb3","datavalue":{"value":"1511.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6045007$5DBFB7E1-7D79-4CA3-B78C-7B91D4640A3A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"85b78ef60851ef0850dc60966a9c25c262e3c898","datavalue":{"value":"10.1007/978-3-319-96145-3_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6045007$EBC8D6D8-E148-4446-891B-83C3B27B065C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0148a7914729f10791714961eacfb31054def7ce","datavalue":{"value":{"entity-type":"item","numeric-id":436614,"id":"Q436614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$8ADD7DFB-2BB6-4D5C-AD90-843EB08B1B23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9402163f6499a1d088bfc900c18810df19851ad9","datavalue":{"value":{"entity-type":"item","numeric-id":526772,"id":"Q526772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$069B3B27-F281-42DA-9898-866EBC0340D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"52faa34d368089f3755999ac6d0e74e76053bd83","datavalue":{"value":{"entity-type":"item","numeric-id":2050105,"id":"Q2050105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$E961CBDF-518C-47DF-A05F-B0ED36AA0540","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"90e86e0413bb4a5005e2255b4afa3c6cabf90b34","datavalue":{"value":{"entity-type":"item","numeric-id":2050106,"id":"Q2050106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$D584C853-0703-40CF-9B8F-C0CE5BE23E56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"acc6f1d0fad50a53047b6dc1f315380bfeb1859f","datavalue":{"value":{"entity-type":"item","numeric-id":2050107,"id":"Q2050107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$6EF5C2D3-EDCE-4D0C-9320-FB455D7C6A6B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d4ba228bb5693c2e3eb7592c46c7d713183c8c65","datavalue":{"value":{"entity-type":"item","numeric-id":2864836,"id":"Q2864836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$564628DE-9B9C-438E-BBB0-384C14BB3CE8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9e202514302232ff7f5ec81097f072c587f02b43","datavalue":{"value":{"time":"+2023-05-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":"Q6045007$112FC8EA-9D9C-4633-8E52-D79944FF8B35","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e574c125a942678b66af570ceca74533aa2d50fa","datavalue":{"value":"https://arxiv.org/abs/1804.05507","type":"string"},"datatype":"url"},"type":"statement","id":"Q6045007$22472209-022C-4A73-AD86-02DAF59C3CE4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6045007$3DCDF9D2-633A-4BFB-9E6B-185A1D842567","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6045007$D7B28084-066E-4EF5-BF15-040A7C72B2E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6045007$96921AF9-AF0D-404C-B294-8AD1E348BC14","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"05b894c0e8a1eee3b5fb9b193175b77ece9058d7","datavalue":{"value":"7689213","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6045007$B83447DD-EED3-418B-96F5-8BB5842E0ED9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da9e1556c2fcea0d362972fe609ab0761a0d2f2d","datavalue":{"value":"Skolem functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q6045007$5C66D7AE-5DE0-4AA7-9E5D-D7C0B66431EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66099e696a2c19d271c11a5347ac1363d45c8b06","datavalue":{"value":"synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q6045007$19F5D743-76EA-415C-9790-BB89D3F0E6EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543c7d0ffd0c52aa92a423848e3694a5bcbfca1e","datavalue":{"value":"SAT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q6045007$BE42A82F-B934-4988-867A-012C2B382A29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"776f3ebb465d60f99820dee5839da6d58a1b42b6","datavalue":{"value":"CEGAR-based approach","type":"string"},"datatype":"string"},"type":"statement","id":"Q6045007$5E5E781F-FC32-4944-8EC0-FFCE1EF0D43D","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":"Q6045007$75176852-D66D-4319-A33F-EFAFD75F04B7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be946f02e692896d7a0e357d6887a420cde4b641","datavalue":{"value":{"entity-type":"item","numeric-id":2050108,"id":"Q2050108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0125c79e4e647098ea69c9613c3d64dd5d2c836b","datavalue":{"value":{"amount":"+0.8617478","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$3F90B37E-C24F-4DB3-AD8F-F06078C8405B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17e72f9465f901c35f25aeec50cf5bcbc814ae21","datavalue":{"value":{"entity-type":"item","numeric-id":6132564,"id":"Q6132564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0f064e034e1467de3af4cb81dcaffcbcf5eee77","datavalue":{"value":{"amount":"+0.82834446","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$9063EC6E-264E-42AD-95DE-6316C98488F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ad8143ec1a0e6c6c7b56bfc54c4f8e789aa6b75","datavalue":{"value":{"entity-type":"item","numeric-id":4036702,"id":"Q4036702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56e187e562350fb5674506083fd1af9c8289a843","datavalue":{"value":{"amount":"+0.817374","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$D3337C72-2621-4C89-9283-05B0B80A4579","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce5a3a3a8cc0ee877e41060cc8e4c037ac22fba5","datavalue":{"value":{"entity-type":"item","numeric-id":2432543,"id":"Q2432543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87e6f8ddad9f3f728f552b5cefd0ed86bd21e4ee","datavalue":{"value":{"amount":"+0.80587465","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$D4C78A8D-71C2-496E-A8E2-AF25662ECDF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddb42c4ef10ac9e969c090494172d73496dd4d4c","datavalue":{"value":{"entity-type":"item","numeric-id":3303903,"id":"Q3303903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"009606d77a91cc03d4a4890c06b352c46ad89518","datavalue":{"value":{"amount":"+0.80431986","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$BD55A1F0-2EBD-43D5-A1C8-D69F962B38AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d88e1ddc85f16f6849edb0575b697310b0811a7","datavalue":{"value":{"entity-type":"item","numeric-id":4633560,"id":"Q4633560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98805c2c1d526f3d4bddbc9fef7cd3b1cd42b91b","datavalue":{"value":{"amount":"+0.80064017","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$28400092-4FDD-4846-90B8-AC227F543413","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18208e729ae7fb48954532532b397df8a8984098","datavalue":{"value":{"entity-type":"item","numeric-id":1946416,"id":"Q1946416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9ea4b185594827619ce95c5850b401d0fd185a4","datavalue":{"value":{"amount":"+0.79063654","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$CD24A672-620E-478F-A78A-ED62B99437A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14083303b8ef0362198b060d3b1f1a5bac2c95b8","datavalue":{"value":{"entity-type":"item","numeric-id":4418725,"id":"Q4418725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"973ac7c17e22133938335b5947f05dd54bc9d961","datavalue":{"value":{"amount":"+0.7822243","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$5D2DE52A-3CD0-489C-A90B-B77F508010F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebbf4d55aaed8941fe36f840b281b0beb74dc4ae","datavalue":{"value":{"entity-type":"item","numeric-id":3720476,"id":"Q3720476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd53a36e42cad17b6b2d1b0b20965cf8ab1770f5","datavalue":{"value":{"amount":"+0.7802987","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$0DFF7335-92B2-4F47-8A3E-1DFE71BDE9C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9928946d27528781f75e136aa50acf2c012d6c6","datavalue":{"value":{"entity-type":"item","numeric-id":5539755,"id":"Q5539755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22be80e67470e3dc139ad8e18a05c956d4a17aaf","datavalue":{"value":{"amount":"+0.77981085","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6045007$2BCC799D-58FD-42E7-9E6D-A0727B675F0F","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6045007$BE2CF9B8-EBE3-4B1A-A622-4520DD856B7C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6045007","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6045007"}}}}}