{"entities":{"Q6700837":{"pageid":14419809,"ns":120,"title":"Item:Q6700837","lastrevid":54645749,"modified":"2026-01-29T18:51:49Z","type":"item","id":"Q6700837","labels":{"en":{"language":"en","value":"SAT Competition 2016 Application Track Benchmarks"}},"descriptions":{"en":{"language":"en","value":"Dataset published at Zenodo repository."}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"dae155fd0809a7906855cd4fa50dd7d71bed552b","datavalue":{"value":{"entity-type":"item","numeric-id":56885,"id":"Q56885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6700837$468D170F-1187-4026-BC29-7EAAB171D4BD","rank":"normal"}],"P1459":[{"mainsnak":{"snaktype":"value","property":"P1459","hash":"02b2e1998c065b488cce4bb48e9946a20c9c05fe","datavalue":{"value":"These are the 299 CNF files in DIMACS format from the application track of the SAT competition 2016. Originally the competition advocated 300 benchmarks but sncf_model_ixl_bmc_depth_14.cnf was truncated (terminating zero and many clauses were missing). Thus only 299 valid DIMACS benchmarks were actually made available. This broken benchmark is from a family of SNCF BMC encodins for the bounds 7 to 15. In 2016 no solver solved any of these bounds nor were the bounds 9, 10, 15 solved in the following anniversary track from the SAT competition 2022 by any solver.","type":"string"},"datatype":"string"},"type":"statement","id":"Q6700837$448AD0AB-4058-47F6-93B5-A9A736E4EA1C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8a73bab82aa135ca51a3da86a65a3d05176a030","datavalue":{"value":{"time":"+2024-06-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6700837$EACEFCDB-5B22-4722-A6DA-D083D169E7ED","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"396db362b8f5a55e9aac7b42eacb07e40796d942","datavalue":{"value":{"entity-type":"item","numeric-id":209458,"id":"Q209458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6700837$29BB82BF-CFBA-4746-8EDF-454ECE386645","rank":"normal"}],"P227":[{"mainsnak":{"snaktype":"value","property":"P227","hash":"e321cfb9df2e127f421520eb293f210eb8124dc0","datavalue":{"value":"11430532","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6700837$60522720-80CD-4DFB-8D9D-79D3A71B8825","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"45486af50a64f9e121da91607d4a5791fbffaf77","datavalue":{"value":"10.5281/zenodo.11430532","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6700837$32219379-5F0E-47E5-A9FA-BBA4F3EB0B28","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":"Q6700837$C58259FC-B631-495B-9328-8F2DAE903C91","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"d1e8073b72a070520efd3d14d4b3d2d3d03859e2","datavalue":{"value":{"entity-type":"item","numeric-id":5984635,"id":"Q5984635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6700837$C32A926F-4327-481C-8263-D76161BDA5A0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SAT Competition 2016 Application Track Benchmarks","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/SAT_Competition_2016_Application_Track_Benchmarks"}}}}}