Inductive Inference

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.


The instances have originally been contributed to the DIMACS benchmark set by Mauricio Resende.
[KKRR92] A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Resende. A Continuous Approach to Inductive Inference. Mathematical Programming, Vol. 57, pages 215-238, 1992.