Please wait ...

Benchmark(s) have been added to cart.

Tag has been added.

• Login
• Links
• FAQs
• Contact

Navigation

• Instance
  • Show Instances
• Problem
  • Show Problems
• Show Tags
• Search
• Cart

Encoding sokoban_opt.lp

Name	sokoban_opt.lp
Class Tree	[Root]    Miscellaneous (45)    ASP Contest 09 (45)    Verification and Evaluation Encodings and Tools (38)
Submitter	Martin Gebser
Author	Martin Gebser and Roland Kaminski
Description
Created	2009-03-21 14:53
Modified	2009-05-09 14:36
Languages
Language Features
Compatible Instance Classes
Input Predicates
Output Predicates
Encoding Parameter
Standalone	No
Tags
Attributes
Content	% possible directions direction(up;down;right;left). loc(L1;L2) :- top(L1,L2). loc(L1;L2) :- right(L1,L2). adj(up, L1,L2) :- top(L1,L2). adj(down, L1,L2) :- top(L2,L1). adj(right,L1,L2) :- right(L1,L2). adj(left, L1,L2) :- right(L2,L1). first(S1) :- step(S1), not next(S2,S1) : step(S2). last(S1) :- step(S1), not next(S1,S2) : step(S2). sokoban(L,S) :- sokoban(L), first(S). box(L,S) :- box(L), first(S). % reachable places at timestep k route(L, S) :- sokoban(L,S), not last(S). route(L2,S) :- route(L1,S), step(S), adj(D,L1,L2), not box(L2,S), not last(S). :- push(L1,D,L2,S), not loc(L1). :- push(L1,D,L2,S), not loc(L2). :- push(L1,D,L2,S), not direction(D). :- push(L1,D,L2,S), not step(S). :- push(L1,D,L2,S), last(S). % :- { push(L1,D,L2,S) : loc(L1) : loc(L2) : direction(D) } 0, step(S), not last(S). :- 2 { push(L1,D,L2,S) : loc(L1) : loc(L2) : direction(D) }, step(S), not last(S). :- push(L1,D,L2,S), adj(D,L3,L1), not route(L3,S). :- push(L1,D,L2,S), { adj(D,L3,L1) : loc(L3) } 0. :- push(L1,D,L2,S), not box(L1,S). % push the box zero or more fields into direction D push(L1,D,S) :- push(L1,D,L2,S), L1 != L2. push(L2,D,S) :- push(L1,D,S), adj(D,L1,L2), step(S), not last(S), not push_to(L1,D,S). :- push(L1,D,S), adj(D,L1,L2), box(L2,S). :- push(L1,D,S), { adj(D,L1,L2) : loc(L2) } 0. % the last push is the final location push_to(L1,D,S) :- push(L3,D,L2,S), adj(D,L1,L2). % the sokoban stands behind the pushed box sokoban(L,S2) :- push_to(L,D,S1), next(S1,S2). sokoban(L,S2) :- sokoban(L,S1), loc(L), next(S1,S2), not push(L1,D,L2,S1) : push(L1,D,L2,S1). % put the pushed box at the new location box(L2,S2) :- push(L1,D,L2,S1), next(S1,S2). % all other boxes stay where they are box(L2,S2) :- box(L2,S1), loc(L2), next(S1,S2), not push(L2,D,L1,S1) : push(L2,D,L1,S1). % the goal goal(S) :- box(L,S) : solution(L), step(S). % goal(S2) :- goal(S1), next(S1,S2), not push(L1,D,L2,S1) : push(L1,D,L2,S1). :- last(S), not goal(S). quality(Q) :- Q = { push(L1,D,L2,S) : push(L1,D,L2,S) }. #hide. #show quality(Q).