These are instances which stem from a formulation of Boolean Function
Synthesis Problems in SAT; The instances are described in [KKRR92] and
have been contributed to the DIMACS benchmark set by Mauricio Resende.
Benchmark instances
There is a total of 41 benchmark instances of this problem type
ranging from instances with 66 variables and 186 clauses (the smallest
instance) up to 1728 variables and 24792 clauses (the largest
instance). A more detailed overview over the size of the instances can
be found in the ps-file (72k) (taken from
the DIMACS FTP site, updated version) which gives an overview over
instances from the DIMACS benchmark set.
Instance hardness
In general, the instances appear to be rather easy for local
search. For example, Walksat (with a noise setting of -noise 60 100 as
the command line parameter) solves all instances with the hardest
instance taking on averge roughly 13000 variable flips. On 25 of the
41 instances WalkSAT, on average, even needs less than 1000 variable
flips to find a solution. Nevertheless, complete algorithms have some
more difficulties with these formulae. For example, SATZ (one of the
best performing complete algorithms to date) does not solve one of the
instances within 30 minutes on a Pentium II 300Mhz. Of the complete
solvers, REL_SAT appears to be the best performing complete algorithm
for these instances.
Acknowledgements
The instances have originally been contributed to the DIMACS benchmark
set by Mauricio
Resende.