Logic Life Search

For scripts to aid with computation or simulation in cellular automata.
User avatar
LaundryPizza03
Posts: 490
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: Logic Life Search

Post by LaundryPizza03 » July 16th, 2019, 3:44 am

Macbi wrote:
LaundryPizza03 wrote:I've noticed that searches tend to take longer as I use it more (following logging in.) For example, (7, 3)/17 (<=4 cells), (8, 2)c/18 (3 cells), and many other speeds in this post mostly took under an hour each, but (6, 5)c/18 is taking an unexpectedly long time. I am also running several other searches for several period multiples of c/2 diagonal (all 4 cells), 29c/29o (3 cells), and 15c/25o (3 cells). A search for a 28c/28o took over 3 days, while the previous 4 period multiples of c orthogonal are all in the linked post. A previous attempt to find a (7,3)c/17 was taking forever before it was killed by a power surge. Is this due to a memory leak or the nature of my searches?
I suspect it's just coincidence based on the searches you're making. You could find out by taking a search that takes a reasonable amount of time (like half an hour) and running it repeatedly to see if it gets longer on average. You'd have to not use your computer for anything else at the same time. Also choose an UNSAT problem for testing since they're less variable than SAT instances.
I've noticed that cancelling the searches for period multiples of c/2d sped up an unrelated search program. However, I am not at the point where I am ready to test my hypothesis.

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia

User avatar
Macbi
Posts: 705
Joined: March 29th, 2009, 4:58 am

Re: Logic Life Search

Post by Macbi » July 16th, 2019, 3:50 am

LaundryPizza03 wrote:I've noticed that cancelling the searches for period multiples of c/2d sped up an unrelated search program. However, I am not at the point where I am ready to test my hypothesis.
That sounds like you're running out of RAM or running more searches than you have cores.

wildmyron
Posts: 1307
Joined: August 9th, 2013, 12:45 am

Re: Logic Life Search

Post by wildmyron » July 16th, 2019, 6:24 am

Macbi wrote:
LaundryPizza03 wrote:I've noticed that cancelling the searches for period multiples of c/2d sped up an unrelated search program. However, I am not at the point where I am ready to test my hypothesis.
That sounds like you're running out of RAM or running more searches than you have cores.
Probably worth noting that if you use glucose-syrup as the SAT solver it defaults to using four threads - which means that you quickly run out of available cores if you have multiple searches running. You can either reduce the maximum number of cores glucose is allowed to use with something like --parameters=" -maxnbthreads=2" as an option to glucose, or compile the single-threaded version of glucose and run lls with

Code: Select all

./lls -S glucose
The latest version of the 5S Project contains over 226,000 spaceships. There is also a GitHub mirror of the collection. Tabulated pages up to period 160 (out of date) are available on the LifeWiki.

User avatar
LaundryPizza03
Posts: 490
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: Logic Life Search

Post by LaundryPizza03 » July 16th, 2019, 10:32 am

wildmyron wrote:
Macbi wrote:
LaundryPizza03 wrote:I've noticed that cancelling the searches for period multiples of c/2d sped up an unrelated search program. However, I am not at the point where I am ready to test my hypothesis.
That sounds like you're running out of RAM or running more searches than you have cores.
Probably worth noting that if you use glucose-syrup as the SAT solver it defaults to using four threads - which means that you quickly run out of available cores if you have multiple searches running. You can either reduce the maximum number of cores glucose is allowed to use with something like --parameters=" -maxnbthreads=2" as an option to glucose, or compile the single-threaded version of glucose and run lls with

Code: Select all

./lls -S glucose
What about Lingeling?

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia

wildmyron
Posts: 1307
Joined: August 9th, 2013, 12:45 am

Re: Logic Life Search

Post by wildmyron » July 16th, 2019, 12:25 pm

LaundryPizza03 wrote:What about Lingeling?
I don't use Lingeling myself, but as I understand it Lingeling is single threaded and Plingeling and Treengling is multithreaded. I don't know what the default settings for the parallel solvers are.

I see that the same group has developed and released a new solver: CaDiCaL. It came in second place overall in the SAT 2019 competition. Has anyone tried it out with LLS generated SAT problems?

Elsewhere...
Macbi wrote:
wildmyron wrote:... The lack of check-pointing in LLS is a significant drawback to using it for hard search problems.
Do any of the common SAT solvers offer this feature? If they do then I'll try to support it in LLS.
From a little research I've done on this topic it does not seem to be a feature offered in glucose, lingeling, cryptominisat, CaDiCal, or Z3.
The latest version of the 5S Project contains over 226,000 spaceships. There is also a GitHub mirror of the collection. Tabulated pages up to period 160 (out of date) are available on the LifeWiki.

User avatar
LaundryPizza03
Posts: 490
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: Logic Life Search

Post by LaundryPizza03 » July 17th, 2019, 6:16 pm

I ran the same search (for 25P3H1V0.2) with minimal background 30 times. No significant trend in the runtimes was observed, so there is likely no memory leak.

Code: Select all

#Search: ./lls -S lingeling -b 16 9 -s p3 y1 -p ">0" -r B3/S23
Run	Time (s)
1	3.85746788979
2	4.07765293121
3	4.08597993851
4	4.04527878761
5	3.88988995552
6	4.00408387184
7	3.97709298134
8	4.05018782616
9	3.98873996735
10	3.91733312607
11	3.89555907249
12	4.01545810699
13	4.01777005196
14	3.91079497337
15	3.97334814072
16	4.16530203819
17	4.05560708046
18	3.97634005547
19	4.07387590408
20	4.05667400360
21	3.94961690903
22	3.97158908844
23	3.86338686943
24	4.13190102577
25	4.13171100616
26	4.03055000305
27	3.99674296379
28	4.02020287514
29	3.95191788673
30	4.11056089401
R^2 = 0.0455796345812215

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia

User avatar
LaundryPizza03
Posts: 490
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: Logic Life Search

Post by LaundryPizza03 » July 18th, 2019, 1:56 am

wildmyron wrote:
LaundryPizza03 wrote:What about Lingeling?
I don't use Lingeling myself, but as I understand it Lingeling is single threaded and Plingeling and Treengling is multithreaded. I don't know what the default settings for the parallel solvers are.
My computer's activity monitor reveals that Lingeling tends to fill up the CPU load for one of my four cores, at least for the search I am running. Would using multiple threads speed up the search process if I don't overload my CPU?

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia

wildmyron
Posts: 1307
Joined: August 9th, 2013, 12:45 am

Re: Logic Life Search

Post by wildmyron » July 18th, 2019, 6:14 am

LaundryPizza03 wrote:
wildmyron wrote:
LaundryPizza03 wrote:What about Lingeling?
I don't use Lingeling myself, but as I understand it Lingeling is single threaded and Plingeling and Treengling is multithreaded. I don't know what the default settings for the parallel solvers are.
My computer's activity monitor reveals that Lingeling tends to fill up the CPU load for one of my four cores, at least for the search I am running. Would using multiple threads speed up the search process if I don't overload my CPU?
To be honest, I really don't know. I find performance testing of these SAT solvers very finicky - and not only because they sometimes give wildly different run times for the same input file. Macbi has mentioned that he felt the parallel solvers didn't give a significant performance improvement - so if you have a choice between one parallel solver and multiple single threaded solvers for different search problems, then it is likely that the multiple single threaded solvers is the better option. However, I'm currently doing some testing of cadical performance compared to lingeling and glucose, during which I've noticed that multiple single threaded solvers can impact each others performance - even when there are idle cores (with hyperthreading disabled on a 6-core i5-8500). I suspect this is due to memory bandwidth competition and may be related to the issue which you've seen with slower running searches (which btw is not related to a "memory leak" because any impact of memory leaks, if they do occur, disappears when a process terminates). To be specific, run time for one of my search problems goes from 8s to 10s, and then to 16s with 1, 2, and 4 instances of the solver running concurrently. That's with at least 2 idles cores.

In any case, here are some timing results from my testing with glucose (v4.1 simp), lingeling (bcj), and cadical (v1.0.3). These are searches oriented towards the 5S project. I don't know what the comparison would be like for B3/S23. All solvers built with default configuration, g++ v5.4.0, Ubuntu 18.0.4 running under Windows Subsytem for Linux on Win10, Core i5-8500 CPU @3.0GHz, 16GB RAM. Timing values for all tests given in seconds (except where otherwise indicated), all tests run consecutively on an otherwise idle system. "X" indicates no result with time run in brackets.

Code: Select all

# cnf files generated with
$ ./lls -r pB2ac34567S012345678 -p ">0" -p "<pop>" -s p7 x6 y0 -b <x> <y> [-s D2-] --dry_run --save_dimacs lls_dimacs.cnf
# Solver run with
$ <solver> lls_dimacs.cnf

                                                    glucose
SAT?    pop   dx    P     x     y     -s    glucose -no-pre lingeling cadical
UNSAT   <7    6     7     13    15    D2-   22.5    1       1.5       1
UNSAT   <7    6     7     15    15    D2-   37      1       6         1.5
UNSAT   <7    6     7     13    9           27      1       2         1.5
UNSAT   <7    6     7     14    10          46      1.5     8         3
UNSAT   =7    6     7     11    12          30      1.5     6         3
SAT     =7    6     7     11    13          22      2       20        7
And for 11c/21:

Code: Select all

$ ./lls -r pB234567S012345678 -p "<pop>" -s p21 x11 y0 -b <x> <y> [-s D2-] --dry_run --save_dimacs lls_dimacs.cnf
# Solver run with
$ <solver> lls_dimacs.cnf

                                                    glucose
SAT?    pop   dx    P     x     y     -s    glucose -no-pre lingeling cadical
UNSAT   =3    11    21    13    13    D2-   48      4.5     16        8
SAT     =3    11    21    15    11    D2-   X(3600) X(3600) X(10hr)   150
I have some other results for longer running searches, but they're a bit dubious because of the timing issues I mentioned above. Also I got some SAT solutions when I wasn't expecting them. Whilst trying to verify the solutions I found that --substitute_solution appears to be broken on the develop branch.

Code: Select all

$ ./lls -r B3S23 -p ">0" -s p3 x1 y0 -s D2- -b 14 12 --dry_run --save_dimacs turtle.cnf --save_state turtle.pkl
$ solvers/lingeling turtle.cnf > turtle-ling.txt
$ ./lls --substitute_solution turtle.pkl turtle-ling.txt

x = 16, y = 14, rule = B3/S23
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb!

$ grep "^[sv]" turtle-ling.txt
s SATISFIABLE
v 1 2 3 4 5 6 7 8 9 -10 11 -12 -13 -14 -15 -16 -17 18 -19 20 21 -22 -23 -24 -25
v -26 27 28 -29 30 -31 -32 33 34 35 36 -37 38 39 -40 -41 -42 -43 -44 -45 46 -47
v -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 65 66 67
v 68 69 70 -71 -72 -73 74 -75 76 77 -78 -79 -80 -81 -82 83 84 85 86 87 88 89 90
v 91 92 93 94 95 96 97 98 -99 -100 -101 102 103 -104 105 -106 -107 -108 109 -110
v 111 112 113 114 115 116 -117 -118 -119 120 121 122 123 -124 125 -126 -127 -128
v 129 -130 131 132 133 -134 -135 -136 -137 -138 -139 140 141 -142 143 -144 -145
v -146 147 -148 149 150 151 -152 -153 -154 -155 -156 -157 158 159 160 161 162
v 163 164 165 166 -167 168 169 -170 -171 -172 173 -174 -175 -176 177 -178 179
v 180 181 182 183 -184 -185 -186 -187 -188 -189 190 -191 192 193 -194 -195 -196
v -197 -198 199 200 201 202 203 204 205 206 207 208 209 210 -211 212 213 -214
v -215 -216 -217 -218 219 220 221 222 223 224 -225 -226 -227 -228 229 -230 -231
v -232 233 -234 235 236 237 238 239 240 241 -242 243 -244 -245 -246 -247 -248
v -249 -250 -251 -252 -253 -254 -255 256 257 258 259 260 261 262 263 264 265 266
v 267 -268 -269 -270 -271 -272 -273 274 275 276 277 -278 279 -280 -281 282 283
v 284 285 286 287 288 289 290 -291 -292 -293 294 295 -296 297 -298 -299 300 301
v 302 303 304 305 -306 -307 -308 -309 -310 -311 -312 -313 -314 -315 -316 -317
v -318 -319 -320 -321 322 -323 -324 -325 -326 327 -328 329 -330 -331 -332 -333
v -334 -335 -336 337 -338 -339 -340 -341 -342 343 -344 -345 346 -347 348 -349
v -350 351 352 -353 -354 -355 -356 -357 358 359 -360 361 362 -363 -364 -365 -366
v -367 -368 -369 -370 -371 372 373 374 -375 -376 377 -378 379 380 -381 382 -383
v -384 -385 386 387 -388 -389 -390 391 392 393 394 -395 -396 -397 -398 -399 -400
v -401 -402 -403 -404 -405 -406 -407 -408 -409 -410 -411 412 -413 -414 -415 -416
v -417 -418 -419 420 421 422 -423 -424 -425 426 427 -428 429 430 -431 432 -433
v -434 435 436 -437 -438 -439 -440 441 -442 -443 -444 -445 446 447 448 -449 -450
v -451 -452 -453 -454 455 -456 -457 -458 459 -460 461 -462 -463 464 -465 -466
v -467 -468 469 -470 -471 -472 -473 474 -475 -476 -477 -478 479 0

$ ./lls -r B3S23 -p ">0" -s p3 x1 y0 -s D2- -b 14 12 -S lingeling

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 246
Number of variables: 479
Number of clauses: 32115

Active width: 14
Active height: 12
Active duration: 4

Solving...
Done

Time taken: 1.52312803268 seconds

x = 16, y = 14, rule = B3/S23
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbobbbb$
bboobbbbbbobobbb$
bbooobboobbbobbb$
bbbobbobbbobobbb$
bbooobbobbobbbbb$
bbooobbooobboobb$
bbooobbooobboobb$
bbooobbobbobbbbb$
bbbobbobbbobobbb$
bbooobboobbbobbb$
bboobbbbbbobobbb$
bbbbbbbbbbbobbbb$
bbbbbbbbbbbbbbbb!
The rle returned by --substitute_solution is blank, whereas the solution is not.

Edit to update timing results.

Also, some insight into the glucose times: For all the tests listed except the 11c/21 which gives a SAT result, glucose is spending almost all of it's time in pre-processing (simplifying?). Running the solver with the "-no-pre" option reduces the run times to less than cadical. Very similar behaviour is seen with glucose-syrup. The pre-processing stage runs on one thread, so having 2 or 4 threads makes almost no difference to the total time for these tests. But with the "-no-pre" option there's a reduction in the real time with increasing nthreads (and generally an increase in the total CPU time).

Lingeling also does simplification by default, and disabling it also reduces the run times for the 6c/7 search problems. The reduction is not as dramatic as for glucose (not included in the table)

cadical also does simplification, and once again disabling it reduces the run time for these problems, but the difference is much smaller. I also tried out the separate preprocessing stages which cadical can do. For the SAT 11c/21 search, adding one round of pre-processing with "-P1" reduced the time from 150 to 115 seconds, but adding an additional round increased the time to 170 seconds. Disabling simplification on this problem drastically increased the run time with "-P1" to >600 seconds (aborted).

Unfortunately I don't think this tells us much about whether simplification in glucose and lingeling has a beneficial effect on run time for search problems we are interested in. It would be great to build up a test set of search problems which are hard enough to exercise the solvers sufficiently, but not so hard that they take days to run.

Edit 2:
Whilst trying to verify the solutions I found that --substitute_solution appears to be broken on the develop branch.
Oops, I hadn't converted the solution to the right format.
The latest version of the 5S Project contains over 226,000 spaceships. There is also a GitHub mirror of the collection. Tabulated pages up to period 160 (out of date) are available on the LifeWiki.

User avatar
LaundryPizza03
Posts: 490
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: Logic Life Search

Post by LaundryPizza03 » July 19th, 2019, 3:27 pm

When I ran the 25P3H1V0.2 search again using cadical's default settings, it took around 36 seconds. Adding -P1 reduced the runtime to around 30 seconds, while disabling simplication reduced it to 17 seconds.

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia

User avatar
LaundryPizza03
Posts: 490
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: Logic Life Search

Post by LaundryPizza03 » July 20th, 2019, 4:47 pm

Thanks, it helped me find a 29c/29o and a (6,5)c/18 much faster.

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia

AlephAlpha
Posts: 33
Joined: October 6th, 2017, 1:50 am

Re: Logic Life Search

Post by AlephAlpha » September 5th, 2019, 6:50 pm

Could you add an option to force the first row/column to be nonempty? That might be helpful for long and thin patterns.

User avatar
Scorbie
Posts: 1437
Joined: December 7th, 2013, 1:05 am

Re: Logic Life Search

Post by Scorbie » November 23rd, 2019, 8:32 pm

May I ask a small question regarding SAT-based Life searching in general?
I'm working on a thin wrapper for Life-searching on Z3. It's currently working, but several times slower.
I'm curious if this was your experience with SMT solvers as well, or was it different?
Best wishes to you, Scorbie

User avatar
Scorbie
Posts: 1437
Joined: December 7th, 2013, 1:05 am

Re: Logic Life Search

Post by Scorbie » November 26th, 2019, 8:56 pm

I compiled Windows binaries for some of the SAT solvers here.
(Edit: Due to licensing issues, moved the repo and distributing it as GPLv3. Using it wouldn't be a problem though.)
CryptoMiniSat offers Windows binaries, so didn't include those.
Any questions and comments welcome.
Best wishes to you, Scorbie

Post Reply