- #1

- 2

- 0

Hi guys,

I'm new to logic and have a logic maze to solve.

basically there is a "solver" program which takes in a set of predicates which must be satisfied to obtain a solution. here's a reproduction of the question below:

The routes to the goal in this case are easy to see. The problem for the solver is to find the shortest route. Of course, you can solve the problem yourself; it is less easy to represent it to the automatic solver.

Here is a simple grid, with some small squares blocked out:

There is a robot in square Ad, and he needs to find his way to the goal (G) in square Dd. At each step he can move to any adjacent square (North, South, East or West) but must avoid the blocked ones.

Find the shortest path he can follow.

--------

There are 3 types of things to define: sorts, functions and the clauses (predicates that must be satisfied).

I have defined my sorts as such:

#sorts

row enum: A,B,C,D,E,F.

col enum:a,b,c,d,e,f.

dir enum: up,down,left,right.

---

then the functions:

pos: row,col -> int {partial all_different}

obs: row,col -> bool {print: none}

goal: row,col -> bool {print:none}

start: row,col -> bool {print:none}

next: row,col,dir -> bool{partial print:none}

---

note: partial means that the function may be undefined for certain arguments

all_different means no two arguments give the same value.

---

clauses - this is where I am stuck.

I want to tell the solver that there is a next cell if it is not an obstacle, it is not out of range and the goal has not been reached.

The solution should look something like:

So far, I have define some clauses :

pos(A,d) = 0 .

x=B, y=d -> goal(x,y).

%define obstacles

obs(A,f).

obs(B,a).

obs(B,c).

obs(C,d).

obs(D,b).

obs(D,c).

obs(D,e).

obs(E,b).

obs(E,e).

%there does not exist a pos(x,y) at an obstacle

EST(x), EST(y), EST(pos(x,y)) -> NOT(obs(x,y)).

%this assigns a number to every cell except the obstacles (which is not exactly what i want of course).

---

sorry that it is a long post. any ideas/hints/tips very welcome and appreciated.

thanks!

I'm new to logic and have a logic maze to solve.

basically there is a "solver" program which takes in a set of predicates which must be satisfied to obtain a solution. here's a reproduction of the question below:

The routes to the goal in this case are easy to see. The problem for the solver is to find the shortest route. Of course, you can solve the problem yourself; it is less easy to represent it to the automatic solver.

Here is a simple grid, with some small squares blocked out:

Code:

```
a b c d e f
+-----+-----+-----+-----+-----+-----+
| | | | o | |*****|
A | | | | [:] | |*****|
| | | | / \ | |*****|
+-----+-----+-----+-----+-----+-----+
|*****| |*****| | | |
B |*****| |*****| | | |
|*****| |*****| | | |
+-----+-----+-----+-----+-----+-----+
| | | |*****| | |
C | | | |*****| | |
| | | |*****| | |
+-----+-----+-----+-----+-----+-----+
| |*****|*****| |*****| |
D | |*****|*****| [G] |*****| |
| |*****|*****| |*****| |
+-----+-----+-----+-----+-----+-----+
| |*****| | |*****| |
E | |*****| | |*****| |
| |*****| | |*****| |
+-----+-----+-----+-----+-----+-----+
| | | | | | |
F | | | | | | |
| | | | | | |
+-----+-----+-----+-----+-----+-----+
```

There is a robot in square Ad, and he needs to find his way to the goal (G) in square Dd. At each step he can move to any adjacent square (North, South, East or West) but must avoid the blocked ones.

Find the shortest path he can follow.

--------

There are 3 types of things to define: sorts, functions and the clauses (predicates that must be satisfied).

I have defined my sorts as such:

#sorts

row enum: A,B,C,D,E,F.

col enum:a,b,c,d,e,f.

dir enum: up,down,left,right.

---

then the functions:

pos: row,col -> int {partial all_different}

obs: row,col -> bool {print: none}

goal: row,col -> bool {print:none}

start: row,col -> bool {print:none}

next: row,col,dir -> bool{partial print:none}

---

note: partial means that the function may be undefined for certain arguments

all_different means no two arguments give the same value.

---

clauses - this is where I am stuck.

I want to tell the solver that there is a next cell if it is not an obstacle, it is not out of range and the goal has not been reached.

The solution should look something like:

Code:

```
path | a b c d e f
-----+------------------
A | 0
B | 1 2 3
C | 4
D | 11 5
E | 10 6
F | 9 8 7
```

So far, I have define some clauses :

pos(A,d) = 0 .

x=B, y=d -> goal(x,y).

%define obstacles

obs(A,f).

obs(B,a).

obs(B,c).

obs(C,d).

obs(D,b).

obs(D,c).

obs(D,e).

obs(E,b).

obs(E,e).

%there does not exist a pos(x,y) at an obstacle

EST(x), EST(y), EST(pos(x,y)) -> NOT(obs(x,y)).

%this assigns a number to every cell except the obstacles (which is not exactly what i want of course).

---

sorry that it is a long post. any ideas/hints/tips very welcome and appreciated.

thanks!

Last edited: