## Logic Life Search

For scripts to aid with computation or simulation in cellular automata.

### Re: Logic Life Search

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.
`x = 4, y = 3, rule = B3-q4z5y/S234k5j2b2o\$b2o\$2o!`

LaundryPizza03 at Wikipedia

LaundryPizza03

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

### Re: Logic Life Search

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.

Macbi

Posts: 685
Joined: March 29th, 2009, 4:58 am

### Re: Logic Life Search

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
`./lls -S glucose`
The latest version of the 5S Project contains over 196,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron

Posts: 1209
Joined: August 9th, 2013, 12:45 am

### Re: Logic Life Search

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
`./lls -S glucose`

`x = 4, y = 3, rule = B3-q4z5y/S234k5j2b2o\$b2o\$2o!`

LaundryPizza03 at Wikipedia

LaundryPizza03

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

### Re: Logic Life Search

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 196,000 spaceships. Tabulated pages up to period 160 are available on the LifeWiki.
wildmyron

Posts: 1209
Joined: August 9th, 2013, 12:45 am

### Re: Logic Life Search

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.
`#Search: ./lls -S lingeling -b 16 9 -s p3 y1 -p ">0" -r B3/S23Run   Time (s)1   3.857467889792   4.077652931213   4.085979938514   4.045278787615   3.889889955526   4.004083871847   3.977092981348   4.050187826169   3.9887399673510   3.9173331260711   3.8955590724912   4.0154581069913   4.0177700519614   3.9107949733715   3.9733481407216   4.1653020381917   4.0556070804618   3.9763400554719   4.0738759040820   4.0566740036021   3.9496169090322   3.9715890884423   3.8633868694324   4.1319010257725   4.1317110061626   4.0305500030527   3.9967429637928   4.0202028751429   3.9519178867330   4.11056089401R^2 = 0.0455796345812215`
`x = 4, y = 3, rule = B3-q4z5y/S234k5j2b2o\$b2o\$2o!`

LaundryPizza03 at Wikipedia

LaundryPizza03

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

### Re: Logic Life Search

wildmyron wrote:

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?
`x = 4, y = 3, rule = B3-q4z5y/S234k5j2b2o\$b2o\$2o!`

LaundryPizza03 at Wikipedia

LaundryPizza03

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

### Re: Logic Life Search

LaundryPizza03 wrote:
wildmyron wrote:

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.
`# 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                                                    glucoseSAT?    pop   dx    P     x     y     -s    glucose -no-pre lingeling cadicalUNSAT   <7    6     7     13    15    D2-   22.5    1       1.5       1UNSAT   <7    6     7     15    15    D2-   37      1       6         1.5UNSAT   <7    6     7     13    9           27      1       2         1.5UNSAT   <7    6     7     14    10          46      1.5     8         3UNSAT   =7    6     7     11    12          30      1.5     6         3SAT     =7    6     7     11    13          22      2       20        7`

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

Posts: 1209
Joined: August 9th, 2013, 12:45 am

### Re: Logic Life Search

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.
`x = 4, y = 3, rule = B3-q4z5y/S234k5j2b2o\$b2o\$2o!`

LaundryPizza03 at Wikipedia

LaundryPizza03

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

### Re: Logic Life Search

Thanks, it helped me find a 29c/29o and a (6,5)c/18 much faster.
`x = 4, y = 3, rule = B3-q4z5y/S234k5j2b2o\$b2o\$2o!`

LaundryPizza03 at Wikipedia

LaundryPizza03

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

Previous