Hacker News new | ask | show | jobs
by Laakeri 2364 days ago
SAT competition 2018 http://sat2018.forsyte.tuwien.ac.at/index.php had a track with random instances. The article "Generating the Uniform Random Benchmarks" in https://helda.helsinki.fi/bitstream/handle/10138/237063/sc20... contains the descriptions of the random instances used.
2 comments

Thanks for the link, but it seems difficult to answer the question "find a SAT instance with no more than 100 variables which all competing solvers failed to solve in the allowed time" from the information presented here.

I'm going to download the benchmarks and try to correlate them with the results CSV table (which doesn't show number of variables for each instance), but since the full random benchmarks are 2.9 GB compressed this might take a fair amount of work.

If you can provide any further guidance on finding the relevant instances I'd appreciate it.

Also note that just specifying the number of variables may not be terribly informative if you don't also specify the maximum clause size and the number of clauses.

For example I see some instances here with 120 variables but they are 7-SAT with around 10k clauses. Unless I'm mistaken reducing those to <=3-SAT will require adding about 20k more variables and tripling the number of clauses.