ILASP currently supports 4 types of ASP rules: normal rules, choice rules, hard constraints and weak constraints. Each type of rule is outlined in the subsections below. There are many other types of ASP rules supported by ASP solvers such as Clingo, and it is possible that future versions of ILASP may support these.
The following Context-free grammar specifies the literals which are permitted in ILASP.
basic_symbol -> [a-z][a-zA-Z0-9_]*
variable -> [A-Z][a-zA-Z0-9_]*
integer -> -?[1-9][0-9]*
bin_op -> '+' | '-' | '*' | '/'
bin_comp -> '<' | '<=' | '=' | '!=' | '>' | '>='
literal -> atom
literal -> 'not ' atom
literal -> term bin_comp term
atom -> basic_symbol
atom -> basic_symbol '(' terms ')'
term -> functional_term
term -> arithmetic_expr
term -> string
functional_term -> basic_symbol
functional_term -> basic_symbol '(' terms ')'
terms -> term
terms -> terms ',' term
arithmetic_expr -> variable
arithmetic_expr -> integer
arithmetic_expr -> arithmetic_expr bin_op arithmetic_expr
arithmetic_expr -> '(' arithmetic_expr ')'
A normal rule is of the form:
h :- b_1, ..., b_n.
where h is an atom and b_1, …, b_n, are literals.
A disjunctive rule is of the form:
h_1 ; ... ; h_m :- b_1, ..., b_n.
where h_1, …, h_m are atoms and b_1, …, b_n, are literals.
A choice rule is of the form:
lb { h_1; ...; h_m } ub :- b_1, ..., b_n.
where lb and ub are integers, h_1, …, h_m are atoms and b_1, …, b_n, are literals.
A hard constraint is of the form:
:- b_1, ..., b_n.
where b_1, …, b_n, are literals.
A weak constraint is of the form:
:~ b_1, ..., b_n.[wt@lev,t_1,...,t_m]
where b_1, …, b_n, are literals, wt and lev are arithmetic
expressions and t_1, …, t_m are terms.
Consider the following ASP background knowledge for the Sudoku task.
cell((1..4,1..4)).
% Note that the '..' notation can be used to define a range of atoms. In
% this case 16 cell atoms are defined.
block((X, Y), tl) :- cell((X, Y)), X < 3, Y < 3.
block((X, Y), tr) :- cell((X, Y)), X > 2, Y < 3.
block((X, Y), bl) :- cell((X, Y)), X < 3, Y > 2.
block((X, Y), br) :- cell((X, Y)), X > 2, Y > 2.
same_row((X1,Y),(X2,Y)) :- X1 != X2, cell((X1,Y)), cell((X2, Y)).
same_col((X,Y1),(X,Y2)) :- Y1 != Y2, cell((X,Y1)), cell((X, Y2)).
same_block(C1,C2) :- block(C1, B), block(C2, B), C1 != C2.
The above program defines a 4x4 Sudoku grid of the form:
#-------#-------#
| : | : |
| - + - | - + - |
| : | : |
#-------#-------#
| : | : |
| - + - | - + - |
| : | : |
#-------#-------#
It also defines what it means for two distinct cells to be in the same
row, column or block as each other.
From ILASP 3.6.0 onwards, conditional literals are supported, meaning
that any literal lit in the above rules (including atoms in the head
of a rule) can be replaced with lit : c_1, ..., c_n, where c_1, …,
c_n are literals. To denote the end of a literals conditions, ;
should be used in place of ,.