# 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:
- Generate
*m* random *k*-clauses. For each clause:
- Select at random
*k* distinct variables from the set of
*n*.
- Negate each with probabilty 1/2. These form the literals of
the clause.

- 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