Concept Definitions involving Aggregates

[GregGelfond]

I have a question on how to define a concept using an aggregate expression. Consider the following declarations for a sudoku model:

Row goes from 1 to 9.

Column goes from 1 to 9.

Value goes from 1 to 9.

grid_square goes from 1 to 9.

A cell is identified by a row, and by a column, and has a grid_square.

Defining the choice rule assigning values to cells is straightforward:

Every cell must be assigned exactly 1 value.

Now suppose I want to define an auxiliary predicate has_duplicates. Intuitively I would like to say something like the following:

A row R has_duplicates when the number of cells with row equal to R assigned value V is greater than 1.

This last statement however gives the following syntax error:

Parser error at line 14, col 54. Unexpected char "v":
r of cells with row equal to R assigned value V is greater than 1.
                                        ^
Expected one of:
 * END_OF_LINE
 * WHERE
 * WHEN
 * AND
 * WHENEVER
 * COMMA

Is there a way to define such an auxiliary predicate using CNL?

[GregGelfond]

Ideally there should be a way to write something like this:

A row R has_duplicates when the number of cells with row equal to are that are assigned value V is greater than 1.

Which intuitively ought to compile to this (if I remember my syntax for aggregates correctly):

has_duplicates(R) :- row(R), #count{ C : cell(C, R, _), assigned(C, V) } > 1.

[simocaruso]

The following should work:

A row is identified by an id.
A column is identified by an id.
A cell is identified by a column, and by a row.
A value is identified by a number.

Every cell can be assigned to exactly 1 value.
A row R has_duplicates whenever we have that the number of columns C that are assigned with row R to value V is greater than 1.

[GregGelfond]

Thanks. First, I made a mistake in my original ASP translation, the concept of duplicates really should be:

has_duplicates(R) :-
    row(R),
    value(V),
    #count{ C : cell(C,R,_) assigned(C, V) } > 1.

The wording should be something like this (intuitively, not necessarily CNL):

A row R has_duplicates if there is a value V where the number of cells with row R assigned V is greater than 1.

The wording you have is a bit strange in some ways. I'm going to try to break it down to get at why, and what I mean:

A row is identified by an id.
A column is identified by an id.
A cell is identified by a column, and by a row.
A value is identified by a number.

Every cell can be assigned to exactly 1 value.

A row R has_duplicates whenever we have that the number of columns C that are assigned with row R to value V is greater than 1.

Here, the definition of has_duplicates counts the number of columns C that are assigned with row R to value V. This seems incorrect for a couple of reasons:

1. Columns and rows are treated independently, and not as constituents of a cell.
2. The relation assigned to is between a cell and a value. The wording doesn't make use of this signature (seemingly).
3. The wording also seems to make it seem that columns are assigned to rows and values.

Do you have an example of a sudoku encoding in CNL?

[GregGelfond]

Here is another attempt:

Row goes from 1 to 9.
Column goes from 1 to 9.

A cell is identified by a column, and by a row.

Value goes from 1 to 9.

Every cell can be assigned to exactly 1 value.

It is prohibited that 
    a cell with row R and column C1 is assigned value V, and also
    a cell with row R and column C2 is assigned value V where
    C1 is different from C2.

Here I'm not attempting to use an aggregate, but a simple constraint:

:- cell(R,C1),
   cell(R,C2),
   assigned(R,C1,V),
   assigned(R,C2,V),
   C1 != C2.

[simocaruso]

Here, the definition of has_duplicates counts the number of columns C that are assigned with row R to value V. This seems incorrect for a couple of reasons:

1. Columns and rows are treated independently, and not as constituents of a cell.
2. The relation assigned to is between a cell and a value. The wording doesn't make use of this signature (seemingly).
3. The wording also seems to make it seem that columns are assigned to rows and values.

Yes columns and rows are treated independently and also 'assigned to' assumes the attributes of cell independently, that is probably why it seems a bit strange.

Here is another attempt:

Row goes from 1 to 9.
Column goes from 1 to 9.

A cell is identified by a column, and by a row.

Value goes from 1 to 9.

Every cell can be assigned to exactly 1 value.

It is prohibited that 
    a cell with row R and column C1 is assigned value V, and also
    a cell with row R and column C2 is assigned value V where
    C1 is different from C2.

Here I'm not attempting to use an aggregate, but a simple constraint:

:- cell(R,C1),
   cell(R,C2),
   assigned(R,C1,V),
   assigned(R,C2,V),
   C1 != C2.

The following should work:

Row goes from 1 to 9.
Column goes from 1 to 9.
A cell is identified by a column, and by a row.
Value goes from 1 to 9.
Every cell can be assigned to exactly 1 value.

It is prohibited that a cell with row R, with column C1 is assigned to value V and also a cell with row R, with column C2 is assigned to value V where C1 is different from C2.