[SMT-LIB] License for the benchmarks

Leon Planken L.R.Planken at tudelft.nl
Wed Feb 23 05:50:48 EST 2011


Hello list,

Are the benchmarks in SMT-LIB made available under some license?
For the specific benchmarks I mean [1], no information is included in the smt
files at least, and I can't find general information on the site either.

More to the point: would there be any problem with distributing graphs
derived from these SMT files under a Creative Commons license (CC-BY or
CC-BY-SA), of course making reference to SMT-LIB and the original benchmarks?

Background:

As a PhD student at Delft University of Technology, I am interested in
developing algorithms for the STP (Simple Temporal Problem), which are
strongly related to computing shortest paths in a directed graph.  I test
these algorithms on, amongst other things, benchmarks derived from QF_IDL
SMT-LIB benchmarks.  I then generate STP instances (graphs) by first randomly
selecting a literal from each SMT clause and then modifying the constraint
weights such that the graph contains no negative cycle, leaving the graph
structure intact.

To make our results reproducable, I would like to make these graph benchmarks
publicly available.

Best regards,
Léon Planken

[1] from version 1.2, QF_IDL: diamonds, DTP, and job_shop.


-- 
I really didn't foresee the Internet. But then, neither did
the computer industry. Not that that tells us very much, of
course - the computer industry didn't even foresee that the
century was going to end.   --  Douglas Adams (1952 - 2001)


More information about the SMT-LIB mailing list