[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