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.


The instances have originally been contributed by Daniele Pretolani to the DIMACS benchmark set.