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 sumfree. By sumfree, 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 sumfree 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 sumfree. 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 
