Details of the Random-k-SAT instances are given in the table below.
The second type of instances were generated from the Random-k-SAT instances. For each Random-3-SAT instance C, one backbone-minimal sub-instance of C was found. This was done by removing clauses from C such that the backbone was unaffected. This was iterated until the resulting instance was backbone-minimal. At each step the removed clause was selected at random from those whose removal did not affect the backbone. Details of these instances are given in the table. The number of clauses varies since the generation process can stop after a varying number of clause removals.
[SGS00] used these instances as part of a study which aimed to explain why cost for local search algorithms was high in the threshold region of Random-3-SAT. For the local search algorithm WSAT/SKC, the backbone-minimal sub-instances had a far higher search cost than the Random-3-SAT instances from which they were derived, even though the sub-instances have fewer clauses, the same backbone size and at least as many solutions.
|test-set||instances||literals per clause||vars|| clauses
|| RTI_k3_n100_m429 || 500 || 3 || 100 || 429|| BMS_k3_n100_m429 || 500 || 3 || 100 || varies|
Random-3-SAT (RTI) and backbone minimal sub-instance (BMS) test-sets. Each instance in the Random-3-SAT collection has a corresponding backbone minimal sub-instance in the other collection. All instances are satisfiable.
|| Josh Singer, Ian Gent and Alan Smaill
Backbone Fragility and the Local Search Cost Peak.
Journal of Artificial
Intelligence Research, 12: 235-270 2000|