Backbone-minimal Sub-instances

The Backbone and Backbone-minimality

A literal l is entailed by a satisfiable SAT instance C iff C AND (NOT l) is unsatisfiable. The backbone of a satisfiable SAT instance is the set of entailed literals and so the backbone size is the number of entailed literals.An instance C is backbone-minimal if for each clause c in C there exists a literal l in the backbone of C such that l is not in the backbone of C - {c} (C with c removed).

Instance Generation

Two types of instance are provided. Firstly, some standard satisfiable threshold Random-k-SAT instances. These are generated according to 3 parameters: k: the number of literals per clause, n: the number of variables, m: the number of clauses. Each Random-k-SAT instance is generated as follows:
  1. Generate m random k-clauses. For each clause:
  2. If the instance is unsatisfiable, restart the generation process.

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.


Bibliography

[SGS00] Josh Singer, Ian Gent and Alan Smaill Backbone Fragility and the Local Search Cost Peak. Journal of Artificial Intelligence Research, 12: 235-270 2000