Class Tree
Description Problem description
===================

The input of the Schur number problem consists of two integers m and n. We need to distribute integers from 1 to n to m disjoint sets so that all of the sets are sum-free. By sum-free, we mean if x and y both belong to the set, then x+y is not in the set.

In our version of the Schur number problem, we have an extra input
which specifies the assignment of the first k integers to sets. The
task then is to check if the given partial assignment can be extended to
a full sum-free assignment.

In this suite of instances, we set m to 5 and n to 130. For instances in the SAT category we have k=15. For instances in the UNSAT category, we have k=20.


Input Format
============

Each input is stored in a plain text file. The format of the file is as follows:

a. The first line is a comment that records the seed we used to generate
the instance. It should be discarded by the ASP system.

b. The next 130 lines define the numbers from 1 to 130 using a unary
predicate called "number". For example:
number(1).
...
number(130).

c. The next 5 lines define the five sets using the unary predicate "part"
part(1).
part(2).
part(3).
part(4).
part(5).d. The next k lines define the assignment of the first k integers. The
prediate name is "assigned". The predicate takes two parameters (x,y).
Therefore, assigned(x,y) means integer x is assigned to set y. For
example:
assigned(1,1).
assigned(2,1).
assigned(3,1).
...

We guarantee that the partial assignment is always sum-free.


Output Requirement
==================

The solution must be represented by means of a binary predicate "inpart".
That is atoms of the form "inpart(x,y)" must describe that integer x
belongs to set y. The solution must coincide with the partial assignment
given in the input.

Authors: Lengning Liu and Miroslaw Truszczynski
Affiliation: University of Kentucky
Email: {lliu1, mirek}@cs.uky.edu
Encodings
1 - 4 of 4