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.
Benchmark instances
There are eight benchmark instances of this class; four instances of
either 60 or 150 propositional variables, see Table 1 for
details.
| instance |
vars |
clauses |
satisfiable? |
| pret60_xx.cnf |
60 |
160 |
yes |
| pret150_xx.cnf |
150 |
400 |
yes |
Table 1: Instances from two-colouring a graph, forced to be unsatisfiable.
Acknowledgements
The instances have originally been contributed by Daniele Pretolani to
the DIMACS benchmark set.