{"entities":{"Q6589830":{"pageid":14200987,"ns":120,"title":"Item:Q6589830","lastrevid":42367176,"modified":"2025-06-13T06:43:31Z","type":"item","id":"Q6589830","labels":{"en":{"language":"en","value":"Truncating abstraction of bit-vector operations for BDD-based SMT solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7898944"}},"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":"Q6589830$C9D877D2-F894-4277-90FB-6DB058D70572","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5daa22a467484810b3eddd550bc658a34bbc4990","datavalue":{"value":{"text":"Truncating abstraction of bit-vector operations for BDD-based SMT solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6589830$57815D1D-805F-4327-9481-886801CD9438","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9ddb4098032df6ce539b1158bb4b49fd29d7ae1d","datavalue":{"value":{"entity-type":"item","numeric-id":831941,"id":"Q831941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$7B8190F9-74AD-4B75-895A-F8D0ACFA44EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"952e13cf13a37e2b25a37008848ccc82d63b7b29","datavalue":{"value":{"entity-type":"item","numeric-id":832316,"id":"Q832316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$B5317C7C-A65C-46CC-92DA-DE9D6826DE06","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$3C37E428-7A83-4B75-8D3A-9A05111F970C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3ac5a36ab43e3a34b30d87cbbbc4e56173ed434d","datavalue":{"value":{"time":"+2024-08-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6589830$98BEC3DA-9D01-49DA-B8B3-8E9BE5803EED","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6589830$575E00FA-5B56-46BE-8711-B6EDD06F2597","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2e1e7e6bfd8041000dd0e1572a7b42e802ffda73","datavalue":{"value":"7898944","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6589830$1670E314-7105-49F6-8A32-2453F27C6D91","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dac36a0d5bcef050bd5c5ec480998b0eb01458a6","datavalue":{"value":"SMT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6589830$370C7952-04E4-445E-95E1-52DBC76D0CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2d9b3c3f716fa4bae84586bb8cf0e7ce4470f70b","datavalue":{"value":"bit-vector theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6589830$BD843285-DC1C-4254-8574-667E17E07379","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"79d20a5ac6b7eea4d5d4582a87fbb29fd268b0b5","datavalue":{"value":"operation abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6589830$BB66BACE-206E-4299-82A0-9442A012CE9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eccdecd9b7d5be1de081282c54765568e2bdd51d","datavalue":{"value":"Q3B","type":"string"},"datatype":"string"},"type":"statement","id":"Q6589830$9737AA1C-1B65-4AD2-A7DE-05C345B4300E","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":"Q6589830$2D9DE8EE-14FC-4DCF-AD3B-F2D30F222C85","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a5f7ec14119349332290c2a3236ae73e2231fc2","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$AB1797E8-52EA-454A-99E8-490D8DD65E59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$DBCA9A33-00FD-45E3-8120-F1082E3E47A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e02764000263ac2bd713cb34d20c92a22d74bf22","datavalue":{"value":{"entity-type":"item","numeric-id":5375393,"id":"Q5375393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$FD1EF72E-F8DF-431A-BD64-6A3FCE557BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3eb85f158fd0145c4ed4d2ff8f13fd27b67d63cb","datavalue":{"value":{"entity-type":"item","numeric-id":2248069,"id":"Q2248069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$FD8C96DE-C16B-4BF9-BA51-3B7178A5C4DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"171f2f23484cc563361b9a949250d7cf0cf0889e","datavalue":{"value":{"entity-type":"item","numeric-id":2479551,"id":"Q2479551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$9BE6C45D-C0D0-4331-8342-9D9FC2A6E405","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"705eb07356f3c57b6af5ee5160fdf7a239743339","datavalue":{"value":{"entity-type":"item","numeric-id":3600470,"id":"Q3600470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$9D4224F3-01E0-43CB-A3E7-7279F00692E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f94ecc0a77f40cc24a1db27854603b882b5e79b","datavalue":{"value":{"entity-type":"item","numeric-id":2818019,"id":"Q2818019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$8C26D249-D728-48CB-8B94-1F57C7706277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57180b9f76f66c808ad1a480880b0280ded3b2ff","datavalue":{"value":{"entity-type":"item","numeric-id":1680265,"id":"Q1680265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$D199FBFB-B59E-4394-A8E0-AF502911B856","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d728259487856e427a26847b7d928d80a254ea62","datavalue":{"value":{"entity-type":"item","numeric-id":1623140,"id":"Q1623140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$E8DBB598-3504-4ECA-A827-0CC9C60FE745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1090c0923a648c9a11d5455265fee31d46be151a","datavalue":{"value":{"entity-type":"item","numeric-id":504997,"id":"Q504997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$32D5AA9F-4108-4C5D-9A00-B40290767A5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"011fd911330c176d4f644d0d384d2eb0c583ecf8","datavalue":{"value":{"entity-type":"item","numeric-id":6039405,"id":"Q6039405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$1C432579-BC8D-43FC-8679-24D8108B3644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81c9773cc9e296251e233b285f6519945481d5eb","datavalue":{"value":{"entity-type":"item","numeric-id":3303898,"id":"Q3303898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$C6886EE0-1D18-4C1D-A56A-8FE475BC1EF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f0c92d03289446e128e8c1b5528c6f94929a65a","datavalue":{"value":{"entity-type":"item","numeric-id":5255085,"id":"Q5255085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$EA84A43F-5BF6-4B7E-9CFD-AD905FC04373","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1cf1fbb097a93619e873e24271fa9638a00cf8d","datavalue":{"value":{"entity-type":"item","numeric-id":2441770,"id":"Q2441770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$14914618-3E3C-40E1-9141-F1535AC459C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a3d8be39100c65d1e448187a4dbf9fe46245230","datavalue":{"value":{"entity-type":"item","numeric-id":2818018,"id":"Q2818018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589830$A1543B5F-B6FF-46BB-9E22-975B57A56392","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"20675c531f7ad94c476ad49f2205a1f615d73174","datavalue":{"value":"10.1016/J.TCS.2024.114664","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6589830$BC50662C-B364-4040-A4E8-22CB17DFBF33","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6589830","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6589830"}}}}}