{"entities":{"Q7361924":{"pageid":31521311,"ns":120,"title":"Item:Q7361924","lastrevid":105370400,"modified":"2026-10-07T13:39:09Z","type":"item","id":"Q7361924","labels":{"en":{"language":"en","value":"An Incremental Simplex Algorithm with Unsatisfiable Core Generation"}},"descriptions":{"en":{"language":"en","value":"AFP entry Simplex"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e7801fe25727e32560bdfdcb443f8f628266d0b7","datavalue":{"value":"https://isa-afp.org/entries/Simplex.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361924$8AD036C9-F7B1-41AB-AB2D-B296547D341D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"13cdd6edc13ae30df49ead881dcc6c954c3f5ea5","datavalue":{"value":{"time":"+2018-08-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361924$9B181ECB-BEA5-497F-BBAC-B35F44759848","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0e4fb94c1160efccb70143a2320bfed556de9d2a","datavalue":{"value":"Filip Mari\u0107","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361924$51C27052-1EDC-4C4D-B76D-BFFDDFFDAC70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e4037ec851632722b0f72289d3f6be0acd4f9a88","datavalue":{"value":"Mirko Spasi\u0107","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361924$1E816EF1-FD58-43EC-86E6-96CA32C1FFF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361924$802504F2-87D0-4BCC-8E62-36FAEFDCC922","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"260e830c64686f1ac4afd609075de835881c541b","datavalue":{"value":{"text":"An Incremental Simplex Algorithm with Unsatisfiable Core Generation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361924$A777F089-AF12-4B96-AF45-DC3594BC00B2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4f5770b61a3c04fb93a2797f84c9ed877bf3d8e6","datavalue":{"value":"We present an Isabelle/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. It supports extraction of satisfying assignments, extraction of minimal unsatisfiable cores, incremental assertion of constraints and backtracking. The formalization relies on stepwise program refinement, starting from a simple specification, going through a number of refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361924$62BC3AAF-060A-4D50-9AE7-F7F9AF088755","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361924$64285B50-37C1-4542-9E31-26C249390FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e386a86950f465930ae0749e91e9486062cb69bc","datavalue":{"value":{"entity-type":"item","numeric-id":4647860,"id":"Q4647860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361924$CA06564B-4363-4309-8D66-69405831C95D","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361924$5B05D30B-089D-49BD-9B59-2BCC3992C8CB","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"b04c93a3ee276587f8dc258d8de827d10d6ade60","datavalue":{"value":{"entity-type":"item","numeric-id":7360780,"id":"Q7360780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361924$333B19D3-DDFE-4C6E-B2FE-3DF9813DD73E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361924$BEB9E27F-EBA1-4F1C-878F-F532CBF2D523","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An Incremental Simplex Algorithm with Unsatisfiable Core Generation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_Incremental_Simplex_Algorithm_with_Unsatisfiable_Core_Generation"}}}}}