Generating Test Cases from Graph Problems

DisLoP Home * mm * dwfs * dwfs_mm * cdwfs

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 syntax that uses ISO Prolog as far as possible but where disjunctions are represented using a predicate disj/2, and negations are represented using not/1, e.g.

a disj b disj c :- not d , e.
a disj b disj d.
bottom :- a,b,c.

Empty clause heads are represented by bottom.

• the syntax of the mm minimal model reasoner that uses "<-" instead of ":-" and represents disjunctions by semicolons, e.g.
a ; b ; c <- d , e.
Empty clause heads are represented by false. Empty clause bodies are represented by true.

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.

To specify the graph that you want to use, select a graph type and then use the parameters to select one specific graph of that type. If you need more information on the graph types and their parameters, please follow this link.
 Graph type: chess simplex subsets allsubs permute parts bintree cliques cycles miles games random rndbipart rndplanar Parameters:

Please select a graph problem to encode. Click here for an overview of the problems available and the encodings of the problems.
 clique domatic number maximal matching vertex coloring vertex cover hamiltonian cycle Parameter:

Format of the output file (see above for details):

Prolog mm style