This system has been developed as a part of the research project DisLoP funded by DFG.
The form below can be used to generate sets of ground clauses which provide interesting test cases for propositional theorem provers. The idea is the following: a graph and an NP-complete problem are selected and then from the graph a set of clauses is generated so that the clause set has a model iff there is a solution for the given problem for this particular graph.
You can choose between two different representations of the clause set:
a disj b disj c :- not d , e.
a disj b disj d.
bottom :- a,b,c.
Empty clause heads are represented by bottom.
Note: The graphs are generated using TheoryBase, a program developed at the University of Kentucky, which creates graphs of different types on the basis of the Stanford GraphBase by D. Knuth.