Skip to content

Commit 562d009

Browse files
gsomixgsomix
committed
wip: SatSolver
1 parent 3414094 commit 562d009

File tree

1 file changed

+153
-86
lines changed

1 file changed

+153
-86
lines changed

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

Lines changed: 153 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ import sttp.client4.upicklejson.default.asJson
44
import upickle.ReadWriter
55

66
import java.nio.file.{Files, Path}
7+
import scala.sys.process.Process
8+
import scala.collection.mutable.ArrayBuffer
79

810
object SatSolver:
911
def solve(problem: ProblemDefinition): Unit =
@@ -69,141 +71,206 @@ object SatSolver:
6971
else
7072
byEnterExit += (enterExit -> (byEnterExit(enterExit) :+ door))
7173

72-
println(s"explored conntection: ${exploredConnections}")
73-
74-
val folder = Files.createTempDirectory(s"icfpc.sat.${problem.name}")
75-
println(s"Temp directory: ${folder}")
74+
println(s"Explored conntections: ${exploredConnections}")
7675

7776
val sb = new StringBuilder()
78-
val roomLabelVariablesCount = problem.size*4
79-
val roomLabelClausesCount = problem.size
8077

81-
val connectionVariablesCount = problem.size*problem.size*6 + problem.size*6
82-
val connectionClausesCount = problem.size*6 + problem.size*problem.size*6
78+
// in case of probatio there are only {0, 1, 2} labels
79+
// for other problems labels are {0, 1, 2, 3}
80+
val labelsCount = if problem.size > 3 then 4 else problem.size
81+
val doorsCount = 6
82+
83+
val roomLabelVariablesCount = problem.size*labelsCount
84+
val connectionVariablesCount = problem.size*problem.size*doorsCount
8385

8486
val variablesCount = roomLabelVariablesCount + connectionVariablesCount
85-
val clausesCount = roomLabelClausesCount + connectionClausesCount
8687
sb ++= s"p cnf ${variablesCount} 9999\n"
8788

88-
// rooms has one of {0, 1, 2, 3} labels
89+
def roomLabelVariableIndex(room: Int, label: Int): Int = room*labelsCount + label + 1
90+
def connectionVariableIndex(roomsCount: Int, enterRoom: Int, exitRoom: Int, door: Int) =
91+
roomLabelVariablesCount + enterRoom*roomsCount*doorsCount + exitRoom*doorsCount + door + 1
92+
93+
// rooms has one of labels
8994
for i <- 0 to problem.size - 1 do
90-
for l <- 0 to 3 do
95+
for l <- 0 to labelsCount - 1 do
9196
sb ++= s"${roomLabelVariableIndex(i, l)} "
9297
sb ++= "0\n"
9398

9499
// but no more one label for the room
95100
for i <- 0 to problem.size - 1 do
96-
for k <- 0 to 3 do
97-
for l <- 0 to 3 do
101+
for k <- 0 to labelsCount - 1 do
102+
for l <- 0 to labelsCount - 1 do
98103
if k < l then
99104
sb ++= s"-${roomLabelVariableIndex(i, k)} "
100105
sb ++= s"-${roomLabelVariableIndex(i, l)} "
101106
sb ++= "0\n"
102107

103108
// all labels should exist
104-
val maxLabel = if problem.size > 3 then 3 else problem.size-1
105-
for l <- 0 to maxLabel do
109+
for l <- 0 to labelsCount - 1 do
106110
for i <- 0 to problem.size - 1 do
107111
sb ++= s"${roomLabelVariableIndex(i, l)} "
108112
sb ++= "0\n"
109113

110114
// for door d should exist at least one connection
111115
for i <- 0 to problem.size - 1 do
112-
for d <- 0 to 5 do
116+
for d <- 0 to doorsCount - 1 do
113117
for j <- 0 to problem.size - 1 do
114-
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, d)} "
118+
sb ++= s"${connectionVariableIndex(problem.size, i, j, d)} "
115119
sb ++= "0\n"
116120

117121
// but no more than one
118122
for i <- 0 to problem.size - 1 do
119-
for d <- 0 to 5 do
123+
for d <- 0 to doorsCount - 1 do
120124
for k <- 0 to problem.size - 1 do
121125
for l <- 0 to problem.size - 1 do
122126
if k < l then
123-
sb ++= s"-${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, k, d)} "
124-
sb ++= s"-${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, l, d)} "
127+
sb ++= s"-${connectionVariableIndex(problem.size, i, k, d)} "
128+
sb ++= s"-${connectionVariableIndex(problem.size, i, l, d)} "
125129
sb ++= "0\n"
126130

127131
// no isolated rooms
128132
for i <- 0 to problem.size - 1 do
129-
for d <- 0 to 5 do
130-
sb ++= s"-${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, i, d)} "
133+
for d <- 0 to doorsCount - 1 do
134+
sb ++= s"-${connectionVariableIndex(problem.size, i, i, d)} "
131135
sb ++= "0\n"
132136

137+
// first room label
138+
val (firstRoomLabel, firstExit, firstDoor) = exploredConnections.head
139+
sb ++= s"${roomLabelVariableIndex(0, firstRoomLabel)} 0\n"
140+
133141
// there is should be at least one back connection OR forward connection should not exist
134142
for i <- 0 to problem.size - 1 do
135143
for j <- 0 to problem.size - 1 do
136-
for d <- 0 to 5 do
137-
sb ++= s"-${roomLabelVariablesCount + connectionVariableIndex(problem.size, i, j, d)} "
138-
for k <- 0 to 5 do
139-
sb ++= s"${roomLabelVariablesCount + connectionVariableIndex(problem.size, j, i, k)} "
144+
for d <- 0 to doorsCount - 1 do
145+
sb ++= s"-${connectionVariableIndex(problem.size, i, j, d)} "
146+
for k <- 0 to doorsCount - 1 do
147+
sb ++= s"${connectionVariableIndex(problem.size, j, i, k)} "
140148
sb ++= "0\n"
141149

142-
// expeditions
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"
150+
// same connections count from room i to j and room j to i
151+
def getBit(number: Int, position: Int): Int =
152+
(number >> position) & 1
151153

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
155-
for i <- 0 to problem.size - 1 do
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"
154+
for i <- 0 to problem.size - 1 do
155+
for j <- 0 to problem.size - 1 do
156+
if i < j then
157+
for k <- 1 to 63 do
158+
for l <- 1 to 63 do
159+
if Integer.bitCount(k) != Integer.bitCount(l) then
160+
for d <- 0 to doorsCount - 1 do
161+
if getBit(k, d) > 0 then
162+
sb ++= s"-${connectionVariableIndex(problem.size, i, j, d)} "
163+
for d <- 0 to doorsCount - 1 do
164+
if getBit(l, d) > 0 then
165+
sb ++= s"-${connectionVariableIndex(problem.size, j, i, d)} "
166+
sb ++= "0\n"
167+
168+
// // expeditions clauses
169+
// for (enter, exit, door) <- exploredConnections do
170+
// if enter != exit then
171+
// // exist connection between two different rooms through the __door__
172+
// for i <- 0 to problem.size - 1 do
173+
// for j <- 0 to problem.size - 1 do
174+
// if i != j then
175+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
176+
// sb ++= "0\n"
177+
178+
// // for enter -door-> exit
179+
// // if room labeled as __enter__ should exist one of connections to other rooms via the __door__
180+
// for (enter, exits) <- byEnter do
181+
// for i <- 0 to problem.size - 1 do
182+
// sb ++= s"-${roomLabelVariableIndex(i, enter)} "
183+
184+
// for (exit, door) <- exits do
185+
// for j <- 0 to problem.size - 1 do
186+
// if enter != exit then
187+
// if i != j then
188+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
189+
// else
190+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
191+
// sb ++= "0\n"
192+
193+
// // if room labeled as __exit__ should exist one of connections from other rooms via the __door__
194+
// for (exit, enters) <- byExit do
195+
// for i <- 0 to problem.size - 1 do
196+
// sb ++= s"-${roomLabelVariableIndex(i, exit)} "
197+
198+
// for (enter, door) <- enters do
199+
// for j <- 0 to problem.size - 1 do
200+
// if enter != exit then
201+
// if i != j then
202+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
203+
// else
204+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
205+
// sb ++= "0\n"
206+
207+
// for ((enter, exit), doors) <- byEnterExit do
208+
// for i <- 0 to problem.size - 1 do
209+
// for j <- 0 to problem.size - 1 do
210+
// if enter != exit then
211+
// if i != j then
212+
// sb ++= s"-${roomLabelVariableIndex(i, enter)} "
213+
// sb ++= s"-${roomLabelVariableIndex(j, exit)} "
214+
// for door <- doors do
215+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
216+
// sb ++= "0\n"
217+
// else
218+
// sb ++= s"-${roomLabelVariableIndex(i, enter)} "
219+
// sb ++= s"-${roomLabelVariableIndex(j, exit)} "
220+
// for door <- doors do
221+
// sb ++= s"${connectionVariableIndex(problem.size, i, j, door)} "
222+
// sb ++= "0\n"
166223

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"
224+
val folder = Files.createTempDirectory(s"icfpc.sat.${problem.name}")
225+
println(s"Temp directory: ${folder}")
180226

181-
for ((enter, exit), doors) <- byEnterExit do
182-
for i <- 0 to problem.size - 1 do
183-
for j <- 0 to problem.size - 1 do
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"
227+
var step = 0
228+
var invalid = true
197229

230+
while invalid && (step < 1) do
231+
invalid = false
232+
step = step + 1
198233

199-
// first room label
200-
val (firstRoomLabel, firstExit, firstDoor) = exploredConnections.head
201-
sb ++= s"${roomLabelVariableIndex(0, firstRoomLabel)} 0\n"
234+
val cnfPath = folder.resolve(s"step${step}.cnf")
235+
val resultPath = folder.resolve(s"step${step}_res.txt")
202236

203-
Files.writeString(folder.resolve("step1.dimacs"), sb.toString)
204-
throw new Exception("Incorrect solution! Analyze results in \"path\".")
237+
Files.writeString(cnfPath, sb.toString)
238+
val process = Process(s"minisat ${cnfPath.toAbsolutePath().toString()} ${resultPath.toAbsolutePath().toString()}")
239+
val exitCode = process.!
240+
241+
val resultLines = Files.readAllLines(resultPath)
242+
val result = resultLines.get(1)
243+
println(s"${result}")
205244

206-
private def roomLabelVariableIndex(room: Int, label: Int): Int = room*4 + label + 1
245+
val solution = result.split(" ").map(_.toInt)
207246

208-
private def connectionVariableIndex(roomsCount: Int, enterRoom: Int, exitRoom: Int, door: Int) =
209-
enterRoom*roomsCount*6 + exitRoom*6 + door + 1
247+
println("Checking if solution is valid...")
248+
for i <- 0 to problem.size - 1 do
249+
for j <- 0 to problem.size - 1 do
250+
if i != j then
251+
var outConnectionsCount = 0
252+
for d <- 0 to 5 do
253+
if solution(connectionVariableIndex(problem.size, i, j, d) - 1) > 0 then
254+
// println(s"out beta(${i}, ${j}, ${d}) = ${solution(connectionVariableIndex(problem.size, i, j, d) - 1)}")
255+
outConnectionsCount = outConnectionsCount + 1
256+
257+
var inConnectionsCount = 0
258+
for d <- 0 to 5 do
259+
if solution(connectionVariableIndex(problem.size, j, i, d) - 1) > 0 then
260+
// println(s"in beta(${j}, ${i}, ${d}) = ${solution(connectionVariableIndex(problem.size, j, i, d) - 1)}")
261+
inConnectionsCount = inConnectionsCount + 1
262+
263+
// println(s"rooms ${i} ${j}, out = ${outConnectionsCount}")
264+
// println(s"rooms ${i} ${j}, in = ${inConnectionsCount}")
265+
if outConnectionsCount != inConnectionsCount then
266+
invalid = true
267+
268+
if invalid then
269+
println("INVALID")
270+
for v <- solution do
271+
sb ++= s"${-v} "
272+
sb ++= "\n"
273+
274+
println(s"Explored conntections: ${exploredConnections}")
275+
println(s"Temp directory: ${folder}")
276+
throw new Exception("Incorrect solution! Analyze results in \"path\".")

0 commit comments

Comments
 (0)