3 lines
4.0 KiB
Plaintext
3 lines
4.0 KiB
Plaintext
# This is the solution file for test_cases\q3\pacphysics_satisfiability2.test.
|
|
pacphysicsAxioms: "((WALL[0,0] >> ~P[0,0]_1) & (WALL[0,1] >> ~P[0,1]_1) & (WALL[0,2] >> ~P[0,2]_1) & (WALL[0,3] >> ~P[0,3]_1) & (WALL[1,0] >> ~P[1,0]_1) & (WALL[1,1] >> ~P[1,1]_1) & (WALL[1,2] >> ~P[1,2]_1) & (WALL[1,3] >> ~P[1,3]_1) & (WALL[2,0] >> ~P[2,0]_1) & (WALL[2,1] >> ~P[2,1]_1) & (WALL[2,2] >> ~P[2,2]_1) & (WALL[2,3] >> ~P[2,3]_1) & (WALL[3,0] >> ~P[3,0]_1) & (WALL[3,1] >> ~P[3,1]_1) & (WALL[3,2] >> ~P[3,2]_1) & (WALL[3,3] >> ~P[3,3]_1) & (P[1,1]_1 | P[1,2]_1 | P[2,1]_1 | P[2,2]_1) & (~P[1,1]_1 | ~P[1,2]_1) & (~P[1,1]_1 | ~P[2,1]_1) & (~P[1,1]_1 | ~P[2,2]_1) & (~P[1,2]_1 | ~P[2,1]_1) & (~P[1,2]_1 | ~P[2,2]_1) & (~P[2,1]_1 | ~P[2,2]_1) & (North_1 | South_1 | East_1 | West_1) & (~North_1 | ~South_1) & (~North_1 | ~East_1) & (~North_1 | ~West_1) & (~South_1 | ~East_1) & (~South_1 | ~West_1) & (~East_1 | ~West_1) & (NORTH_BLOCKED_1 <=> (PWALL[1,1,1,2]_1 | PWALL[1,2,1,3]_1 | PWALL[2,1,2,2]_1 | PWALL[2,2,2,3]_1)) & (SOUTH_BLOCKED_1 <=> (PWALL[1,1,1,0]_1 | PWALL[1,2,1,1]_1 | PWALL[2,1,2,0]_1 | PWALL[2,2,2,1]_1)) & (EAST_BLOCKED_1 <=> (PWALL[1,1,2,1]_1 | PWALL[1,2,2,2]_1 | PWALL[2,1,3,1]_1 | PWALL[2,2,3,2]_1)) & (WEST_BLOCKED_1 <=> (PWALL[1,1,0,1]_1 | PWALL[1,2,0,2]_1 | PWALL[2,1,1,1]_1 | PWALL[2,2,1,2]_1)) & (PWALL[1,1,1,2]_1 <=> (P[1,1]_1 & WALL[1,2])) & (PWALL[1,2,1,3]_1 <=> (P[1,2]_1 & WALL[1,3])) & (PWALL[2,1,2,2]_1 <=> (P[2,1]_1 & WALL[2,2])) & (PWALL[2,2,2,3]_1 <=> (P[2,2]_1 & WALL[2,3])) & (PWALL[1,1,1,0]_1 <=> (P[1,1]_1 & WALL[1,0])) & (PWALL[1,2,1,1]_1 <=> (P[1,2]_1 & WALL[1,1])) & (PWALL[2,1,2,0]_1 <=> (P[2,1]_1 & WALL[2,0])) & (PWALL[2,2,2,1]_1 <=> (P[2,2]_1 & WALL[2,1])) & (PWALL[1,1,2,1]_1 <=> (P[1,1]_1 & WALL[2,1])) & (PWALL[1,2,2,2]_1 <=> (P[1,2]_1 & WALL[2,2])) & (PWALL[2,1,3,1]_1 <=> (P[2,1]_1 & WALL[3,1])) & (PWALL[2,2,3,2]_1 <=> (P[2,2]_1 & WALL[3,2])) & (PWALL[1,1,0,1]_1 <=> (P[1,1]_1 & WALL[0,1])) & (PWALL[1,2,0,2]_1 <=> (P[1,2]_1 & WALL[0,2])) & (PWALL[2,1,1,1]_1 <=> (P[2,1]_1 & WALL[1,1])) & (PWALL[2,2,1,2]_1 <=> (P[2,2]_1 & WALL[1,2])) & (GEQ_1_adj_walls_1 <=> (NORTH_BLOCKED_1 | SOUTH_BLOCKED_1 | EAST_BLOCKED_1 | WEST_BLOCKED_1)) & (GEQ_2_adj_walls_1 <=> ((NORTH_BLOCKED_1 & SOUTH_BLOCKED_1) | (NORTH_BLOCKED_1 & EAST_BLOCKED_1) | (NORTH_BLOCKED_1 & WEST_BLOCKED_1) | (SOUTH_BLOCKED_1 & EAST_BLOCKED_1) | (SOUTH_BLOCKED_1 & WEST_BLOCKED_1) | (EAST_BLOCKED_1 & WEST_BLOCKED_1))) & (GEQ_3_adj_walls_1 <=> ((NORTH_BLOCKED_1 & SOUTH_BLOCKED_1 & EAST_BLOCKED_1) | (NORTH_BLOCKED_1 & SOUTH_BLOCKED_1 & WEST_BLOCKED_1) | (NORTH_BLOCKED_1 & EAST_BLOCKED_1 & WEST_BLOCKED_1) | (SOUTH_BLOCKED_1 & EAST_BLOCKED_1 & WEST_BLOCKED_1))) & (P[1,1]_1 <=> ((~P[1,1]_0 & ~WALL[1,1] & ((P[1,2]_0 & South_0) | (P[2,1]_0 & West_0))) | (P[1,1]_0 & (WALLNorth[1,2]_0 | WALLSouth[1,0]_0 | WALLEast[2,1]_0 | WALLWest[0,1]_0)))) & (WALLNorth[1,2]_0 <=> (WALL[1,2] & North_0)) & (WALLSouth[1,0]_0 <=> (WALL[1,0] & South_0)) & (WALLEast[2,1]_0 <=> (WALL[2,1] & East_0)) & (WALLWest[0,1]_0 <=> (WALL[0,1] & West_0)) & (P[1,2]_1 <=> ((~P[1,2]_0 & ~WALL[1,2] & P[2,2]_0 & West_0) | (P[1,2]_0 & (WALLNorth[1,3]_0 | WALLSouth[1,1]_0 | WALLEast[2,2]_0 | WALLWest[0,2]_0)))) & (WALLNorth[1,3]_0 <=> (WALL[1,3] & North_0)) & (WALLSouth[1,1]_0 <=> (WALL[1,1] & South_0)) & (WALLEast[2,2]_0 <=> (WALL[2,2] & East_0)) & (WALLWest[0,2]_0 <=> (WALL[0,2] & West_0)) & (P[2,1]_1 <=> ((~P[2,1]_0 & ~WALL[2,1] & P[2,2]_0 & South_0) | (P[2,1]_0 & (WALLNorth[2,2]_0 | WALLSouth[2,0]_0 | WALLEast[3,1]_0 | WALLWest[1,1]_0)))) & (WALLNorth[2,2]_0 <=> (WALL[2,2] & North_0)) & (WALLSouth[2,0]_0 <=> (WALL[2,0] & South_0)) & (WALLEast[3,1]_0 <=> (WALL[3,1] & East_0)) & (WALLWest[1,1]_0 <=> (WALL[1,1] & West_0)) & (P[2,2]_1 <=> ((~P[2,2]_0 & ~WALL[2,2] & ((P[2,1]_0 & North_0) | (P[1,2]_0 & East_0))) | (P[2,2]_0 & (WALLNorth[2,3]_0 | WALLSouth[2,1]_0 | WALLEast[3,2]_0 | WALLWest[1,2]_0)))) & (WALLNorth[2,3]_0 <=> (WALL[2,3] & North_0)) & (WALLSouth[2,1]_0 <=> (WALL[2,1] & South_0)) & (WALLEast[3,2]_0 <=> (WALL[3,2] & East_0)) & (WALLWest[1,2]_0 <=> (WALL[1,2] & West_0)))"
|