Controlled Backbone Size Instances

The Backbone

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.

Instance Generation

These instances are satisfiable threshold Random-3-SAT with the backbone size "controlled" at various values. Each collection has 4 parameters to which all instances in the collection conform: k: the number of literals per clause, n: the number of variables, m: the number of clauses, b: the size of the backbone.

Each instance in each collection is generated as follows:

  1. Generate m random k-clauses. For each clause:
  2. If the instance is unsatisfiable, restart the generation process.
  3. Determine the backbone size. If it is not equal to b, restart the generation process.

[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 instances which had the highest search cost are those with a small number of clauses but a large backbone. Cost decreases with a smaller backbone or a larger number of clauses.

test-set instances literals per clause vars clauses backbone size
CBS_k3_n100_m403_b10 1000 3 100 403 10
CBS_k3_n100_m403_b30 1000 3 100 403 30
CBS_k3_n100_m403_b50 1000 3 100 403 50
CBS_k3_n100_m403_b70 1000 3 100 403 70
CBS_k3_n100_m403_b90 1000 3 100 403 90
CBS_k3_n100_m411_b10 1000 3 100 411 10
CBS_k3_n100_m411_b30 1000 3 100 411 30
CBS_k3_n100_m411_b50 1000 3 100 411 50
CBS_k3_n100_m411_b70 1000 3 100 411 70
CBS_k3_n100_m411_b90 1000 3 100 411 90
CBS_k3_n100_m418_b10 1000 3 100 418 10
CBS_k3_n100_m418_b30 1000 3 100 418 30
CBS_k3_n100_m418_b50 1000 3 100 418 50
CBS_k3_n100_m418_b70 1000 3 100 418 70
CBS_k3_n100_m418_b90 1000 3 100 418 90
CBS_k3_n100_m423_b10 1000 3 100 423 10
CBS_k3_n100_m423_b30 1000 3 100 423 30
CBS_k3_n100_m423_b50 1000 3 100 423 50
CBS_k3_n100_m423_b70 1000 3 100 423 70
CBS_k3_n100_m423_b90 1000 3 100 423 90
CBS_k3_n100_m429_b10 1000 3 100 429 10
CBS_k3_n100_m429_b30 1000 3 100 429 30
CBS_k3_n100_m429_b50 1000 3 100 429 50
CBS_k3_n100_m429_b70 1000 3 100 429 70
CBS_k3_n100_m429_b90 1000 3 100 429 90
CBS_k3_n100_m435_b10 1000 3 100 435 10
CBS_k3_n100_m435_b30 1000 3 100 435 30
CBS_k3_n100_m435_b50 1000 3 100 435 50
CBS_k3_n100_m435_b70 1000 3 100 435 70
CBS_k3_n100_m435_b90 1000 3 100 435 90
CBS_k3_n100_m441_b10 1000 3 100 441 10
CBS_k3_n100_m441_b30 1000 3 100 441 30
CBS_k3_n100_m441_b50 1000 3 100 441 50
CBS_k3_n100_m441_b70 1000 3 100 441 70
CBS_k3_n100_m441_b90 1000 3 100 441 90
CBS_k3_n100_m449_b10 1000 3 100 449 10
CBS_k3_n100_m449_b30 1000 3 100 449 30
CBS_k3_n100_m449_b50 1000 3 100 449 50
CBS_k3_n100_m449_b70 1000 3 100 449 70
CBS_k3_n100_m449_b90 1000 3 100 449 90

Table 1: Controlled backbone size test-sets. 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