{"entities":{"Q2151238":{"pageid":2161981,"ns":120,"title":"Item:Q2151238","lastrevid":57749850,"modified":"2026-04-01T06:34:29Z","type":"item","id":"Q2151238","labels":{"en":{"language":"en","value":"Reluplex: an efficient SMT solver for verifying deep neural networks"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7551559"}},"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":"Q2151238$50402547-AFCC-432C-9EE3-09145EA2368F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bd7d1c329606c3ee03ab01bafbdbaea69cad11cc","datavalue":{"value":{"text":"Reluplex: an efficient SMT solver for verifying deep neural networks","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2151238$79F8AB19-4162-4CF4-9BD2-F9511D5FAC7F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"68294dd513dbba6f660714272b8b6e695eb11c64","datavalue":{"value":"1494.68167","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2151238$E54EBD18-4B11-40AD-9FAF-E3702E71A323","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"24380e1d232d42b21badb2064acfeecaef718cbf","datavalue":{"value":"10.1007/978-3-319-63387-9_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2151238$975E1883-DAAB-45D3-967F-86E98FADD168","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"051db72c27a6ffd1dc64c69febb1b92cb862178b","datavalue":{"value":{"entity-type":"item","numeric-id":2151236,"id":"Q2151236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2151238$59643AA8-2676-43B9-B390-BF3CB097990A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2151238$4D3BA988-B0D4-4463-902B-11F3988BF2A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2dd061ef340feff0cbd009fd7ff490684b9da51c","datavalue":{"value":{"entity-type":"item","numeric-id":685109,"id":"Q685109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2151238$732B0FC6-402A-431D-86A3-B977C5AEF9F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b662261780264ff26bb1473dae97172ef612f53","datavalue":{"value":{"entity-type":"item","numeric-id":2151237,"id":"Q2151237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2151238$400E5C0E-8DFA-4BA4-9BFA-56F97BE1C479","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d33cb3cd805d6edbe61572e88ef6f09a93a3d677","datavalue":{"value":{"entity-type":"item","numeric-id":1694947,"id":"Q1694947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2151238$47B7B3E1-6FB8-494B-8F48-D10C22E18D74","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b01f91c2828ea0406533259953e45b7596e1cea7","datavalue":{"value":{"time":"+2022-07-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2151238$952FF6CC-7671-4C86-91CD-E00F15EBC47A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5dfaa1eff3535c2799095b8a2e1bb9dbe71757f5","datavalue":{"value":"https://arxiv.org/abs/1702.01135","type":"string"},"datatype":"url"},"type":"statement","id":"Q2151238$50CF865C-B303-4D41-BE13-25F6B0B1BB34","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2151238$1F49D78E-9ABE-4F46-90E7-DA2E0DAC5FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"86ef24f5c9e2aac48660aa2e36054c8246d3fc97","datavalue":{"value":"68T07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2151238$C97E119D-7583-4EBA-B3BF-39BC66970943","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0a79997b96885e5c49160655f62313814e034e1f","datavalue":{"value":"7551559","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2151238$6FFC931A-E543-49DD-B07F-4CA8FA4F955D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cce6389303f6b97897dfec78f9efcc53ef4b50fe","datavalue":{"value":"deep neural networks (DNNs)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2151238$EFC2DE4D-2164-488E-AD27-DE8F00AF231C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75999b4145baf8e36d1aae9da7d6c1e17358728e","datavalue":{"value":"satisfiability modulo theories (SMT)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2151238$4B38646E-FA47-420E-B1A6-5ACD419BED1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ce3994eb534b696cb9eff647caee14250aaf291c","datavalue":{"value":"rectified linear unit (ReLU)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2151238$74B05BDB-276C-4480-803E-9CD6D8FE993F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"30500396ef75049eeda86e600c6dede99d905ba6","datavalue":{"value":"airborne collision avoidance system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2151238$8E776F02-5BDC-4731-AE79-AEEFEFF19B4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a37e8c6c5b4e115dcbe6de3a8c9b23b22d17cc6b","datavalue":{"value":"ReLU function","type":"string"},"datatype":"string"},"type":"statement","id":"Q2151238$75FA51A6-5B34-405D-9DC3-E99A2394CCC3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fac9f12a57b80383023f1d0f3d27b15b8df1d760","datavalue":{"value":{"entity-type":"item","numeric-id":43078,"id":"Q43078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2151238$6F9A64FB-F2FC-43A0-92D8-0FA3A1223761","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":"Q2151238$35460DBE-B436-486F-845B-8A5D6156D333","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d45acb0c169b6ba65e9d9c48debe6bd897ee6737","datavalue":{"value":"W2594877703","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2151238$A0C628BE-2B72-472A-A0AF-4D0F92F3CAD4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4fb6b3a002d436dca1aca638e99dfa0a760274bf","datavalue":{"value":{"entity-type":"item","numeric-id":3164970,"id":"Q3164970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"297348a7d7a5a89ace8220ce304e363600d47194","datavalue":{"value":{"amount":"+0.932044","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":"Q2151238$8BC8DC92-84EC-4D40-981E-A8D476F2731C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c7594e0bd8e19d030028ffeb913e279a8573504","datavalue":{"value":{"entity-type":"item","numeric-id":2046329,"id":"Q2046329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"709ea368447143016c4c1ffcceda6ae79e17a09c","datavalue":{"value":{"amount":"+0.90143186","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":"Q2151238$8ADD8661-608F-4C9F-B60A-A7BEC0604D37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99f1e56ef15a676956e05c569dd1f1a194309f8b","datavalue":{"value":{"entity-type":"item","numeric-id":2233508,"id":"Q2233508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d66151728e7ae41594a121f81c864f9b1da5906d","datavalue":{"value":{"amount":"+0.8984415","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":"Q2151238$2700A4B1-B8B9-434A-97AB-3AAAF7C6CF59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"086962fca481926d59254c996d595cad5290020e","datavalue":{"value":{"entity-type":"item","numeric-id":2112128,"id":"Q2112128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25f234af0193ad16d482adc28ce47698d9885e1e","datavalue":{"value":{"amount":"+0.898401","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":"Q2151238$62C7A0BD-7B94-4659-A133-852BBB59D2E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80c35f16574fc06d6eccd38fbf10b4591d2b7727","datavalue":{"value":{"entity-type":"item","numeric-id":6108442,"id":"Q6108442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53f6b3b3976b8b10144c0a8092213049ef4e8d6a","datavalue":{"value":{"amount":"+0.89804894","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":"Q2151238$67A85A8F-DCCA-47A2-B680-290793A9F825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdf24e9f721fb827a7be4bf40b8d0b1b20ddec3c","datavalue":{"value":{"entity-type":"item","numeric-id":832168,"id":"Q832168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a09ad03bf0f692f9e4c802c95a4f8ba5ec8f7ab0","datavalue":{"value":{"amount":"+0.8933476","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":"Q2151238$797495E2-FB7D-4601-84F3-B4025B5EFD69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ca5ce011e40c27c175d4f0d9a925083703c6ab4","datavalue":{"value":{"entity-type":"item","numeric-id":2225077,"id":"Q2225077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ceac9afca3de70d77ba0e07c0ffd82ca454967f5","datavalue":{"value":{"amount":"+0.87285113","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":"Q2151238$FD06A2F6-BCCF-4956-AB86-E2C0D26D6B1E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2151238","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2151238"}}}}}