Some instances from 
"Eﬃciently Calculating Evolutionary Tree Measures Using SAT"
Maria Luisa Bonet and Katherine St. John
to appear in SAT 09

The paper uses SAT solvers to calculate interesting biological
measures between phylogenetic trees.  The main measure, the
hybrid number, calculates the minimal number of hybridization
events that transform one tree to another.  For each possible
number, we encode the related maximum agreement forest into 
a SAT instance and then use various SAT solvers to find the 
smallest satisfiable instance.

The biological dataset used in the paper compares phylogenetic
trees (roughly, evolutionary histories) of various genes 
found in the grass family of plants (Schmidt `03), a family
that exhibits high levels of hybridization.

Included in this set of instances are three comparisons for 
which we have lower and upper bounds, but not the exact
answer.   The comparisons are:

ndhf xits:
	Instances 9-14 are unsatisfiable
	Instances 15-19 are unknown
	Instances 20-22 are satisfiable

rbcl xits:
	Instances 6-8 are unsatisfiable
	Instances 9-13 are unknown
	Instances 14-19 are satisfiable

rpoC2 xits:
	Instances 7-9 are unsatisfiable
	Instances 10-14 are unknown
	Instances 15-18 are satisfiable
