Skip to content

Commit b491c1b

Browse files
gsomixgsomix
committed
wip: SatSolver
1 parent 2bbd218 commit b491c1b

File tree

1 file changed

+95
-14
lines changed

1 file changed

+95
-14
lines changed

‎src/main/scala/ru/org/codingteam/icfpc_2025/SatSolver.scala‎

Lines changed: 95 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,14 @@ object SatSolver:
3333
return
3434

3535
private def nextStep(problem: ProblemDefinition, knowledge: KnowledgeHolder): Step =
36+
if knowledge.visitedRoutes.size == 0 then
37+
val plan = Seq(Lanternarius.shuffle12(problem.maxRouteLength))
38+
return Step.ExploreStep(plan)
39+
3640
var exploredConnections = Seq.empty[(Int, Int, Int)]
41+
var byEnter = Map.empty[Int, Seq[(Int, Int)]]
42+
var byExit = Map.empty[Int, Seq[(Int, Int)]]
43+
var byEnterExit = Map.empty[(Int, Int), Seq[Int]]
3744

3845
for j <- knowledge.visitedRoutes.indices do
3946
val plan = knowledge.visitedRoutes(j)
@@ -46,6 +53,22 @@ object SatSolver:
4653

4754
exploredConnections = exploredConnections :+ (enter, exit, door)
4855

56+
if !byEnter.contains(enter) then
57+
byEnter += (enter -> Seq((exit, door)))
58+
else
59+
byEnter += (enter -> (byEnter(enter) :+ (exit, door)))
60+
61+
if !byExit.contains(exit) then
62+
byExit += (exit -> Seq((enter, door)))
63+
else
64+
byExit += (exit -> (byExit(exit) :+ (enter, door)))
65+
66+
var enterExit = (enter, exit)
67+
if !byEnterExit.contains(enterExit) then
68+
byEnterExit += (enterExit -> Seq(door))
69+
else
70+
byEnterExit += (enterExit -> (byEnterExit(enterExit) :+ door))
71+
4972
println(s"explored conntection: ${exploredConnections}")
5073

5174
val folder = Files.createTempDirectory(s"icfpc.sat.${problem.name}")
@@ -68,6 +91,22 @@ object SatSolver:
6891
sb ++= s"${roomLabelVariableIndex(i, l)} "
6992
sb ++= "0\n"
7093

94+
// but no more one label for the room
95+
for i <- 0 to problem.size - 1 do
96+
for k <- 0 to 3 do
97+
for l <- 0 to 3 do
98+
if k < l then
99+
sb ++= s"-${roomLabelVariableIndex(i, k)} "
100+
sb ++= s"-${roomLabelVariableIndex(i, l)} "
101+
sb ++= "0\n"
102+
103+
// all labels should exist
104+
val maxLabel = if problem.size > 3 then 3 else problem.size-1
105+
for l <- 0 to maxLabel do
106+
for i <- 0 to problem.size - 1 do
107+
sb ++= s"${roomLabelVariableIndex(i, l)} "
108+
sb ++= "0\n"
109+
71110
// for door d should exist at least one connection
72111
for i <- 0 to problem.size - 1 do
73112
for d <- 0 to 5 do
@@ -101,27 +140,69 @@ object SatSolver:
101140
sb ++= "0\n"
102141

103142
// expeditions
104-
for (enterLabel, exitLabel, door) <- exploredConnections do
105-
// enter
143+
for (enter, exit, door) <- exploredConnections do
144+
if enter != exit then
145+
// exist connection between two different rooms through the __door__
146+
for i <- 0 to problem.size - 1 do
147+
for j <- 0 to problem.size - 1 do
148+
if i != j then
149+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
150+
sb ++= "0\n"
151+
152+
// for enter -door-> exit
153+
// if room labeled as __enter__ should exist one of connections to other rooms via the __door__
154+
for (enter, exits) <- byEnter do
106155
for i <- 0 to problem.size - 1 do
107-
for j <- 0 to problem.size - 1 do
108-
sb ++= s"-${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
109-
sb ++= s"${roomLabelVariableIndex(i, enterLabel)}"
110-
// exit
156+
sb ++= s"-${roomLabelVariableIndex(i, enter)} "
157+
158+
for (exit, door) <- exits do
159+
for j <- 0 to problem.size - 1 do
160+
if enter != exit then
161+
if i != j then
162+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
163+
else
164+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
165+
sb ++= "0\n"
166+
167+
// if room labeled as __exit__ should exist one of connections from other rooms via the __door__
168+
for (exit, enters) <- byExit do
169+
for i <- 0 to problem.size - 1 do
170+
sb ++= s"-${roomLabelVariableIndex(i, exit)} "
171+
172+
for (enter, door) <- enters do
173+
for j <- 0 to problem.size - 1 do
174+
if enter != exit then
175+
if i != j then
176+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
177+
else
178+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
179+
sb ++= "0\n"
180+
181+
for ((enter, exit), doors) <- byEnterExit do
111182
for i <- 0 to problem.size - 1 do
112183
for j <- 0 to problem.size - 1 do
113-
sb ++= s"-${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
114-
sb ++= s"${roomLabelVariableIndex(j, exitLabel)}"
184+
if enter != exit then
185+
if i != j then
186+
sb ++= s"-${roomLabelVariableIndex(i, enter)} "
187+
sb ++= s"-${roomLabelVariableIndex(j, exit)} "
188+
for door <- doors do
189+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
190+
sb ++= "0\n"
191+
else
192+
sb ++= s"-${roomLabelVariableIndex(i, enter)} "
193+
sb ++= s"-${roomLabelVariableIndex(j, exit)} "
194+
for door <- doors do
195+
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, door)} "
196+
sb ++= "0\n"
197+
198+
199+
// first room label
200+
val (firstRoomLabel, firstExit, firstDoor) = exploredConnections.head
201+
sb ++= s"${roomLabelVariableIndex(0, firstRoomLabel)} 0\n"
115202

116203
Files.writeString(folder.resolve("step1.dimacs"), sb.toString)
117204
throw new Exception("Incorrect solution! Analyze results in \"path\".")
118205

119-
if knowledge.visitedRoutes.size > 0 then
120-
return Step.StopGuessing()
121-
else
122-
val plan = Seq(Lanternarius.lanternarius(problem.maxRouteLength))
123-
return Step.ExploreStep(plan)
124-
125206
private def roomLabelVariableIndex(room: Int, label: Int): Int = room*4 + label + 1
126207

127208
private def connectionVariableIndex(roomsCount: Int, enterRoom: Int, exitRoom: Int, door: Int) =

0 commit comments

Comments
 (0)