Two-colouring a graph, forced to be unsatisfiable
The instances are an encoding of two-colouring a graph, along with a
parity constraint to force unsatisfiability. A generater (trisat.c)
for these instances is available at
this directory of the original DIMACS ftp-site.
There are eight benchmark instances of this class; four instances of
either 60 or 150 propositional variables, see Table 1 for
Table 1: Instances from two-colouring a graph, forced to be unsatisfiable.
The instances have originally been contributed by Daniele Pretolani to
the DIMACS benchmark set.