Diagnosis Benchmark:

This benchmark is based on the Reiter style minimal diagnosis of digital 
circuits [Reiter, 1987] encoded as circumscription [Lifschitz, 1985].  

First a random tree is generated. Input gates (leaves of the tree) are 
assigned a random boolean value, intermediate nodes are assigned a random 
boolean function. The root node of the tree is the output of the circuit. 
The value of the output is calculated and swapped in order to obtain faulty
behaviour for the circuit. 

The encodings are in the internal format of smodels and textual format can 
be produced using the program lplist with options --gnt or --dlv.

Parameters:

The number of nodes in the tree forming the digital circuit N grows from 
18 to 28. There are 20 instances for each number of nodes N.

All atoms "high*" are varied, while an atom "abI" is given priority M for  
minimization (for a number of priorities is K) if

       floor((M-1)*N/K)+1 <= I <= floor(M*N/K).