Page 8 of 13
Re: Logic Life Search
Posted: July 16th, 2019, 3:44 am
by LaundryPizza03
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.
Re: Logic Life Search
Posted: July 16th, 2019, 3:50 am
by Macbi
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.
Re: Logic Life Search
Posted: July 16th, 2019, 6:24 am
by wildmyron
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
Re: Logic Life Search
Posted: July 16th, 2019, 10:32 am
by LaundryPizza03
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
What about Lingeling?
Re: Logic Life Search
Posted: July 16th, 2019, 12:25 pm
by wildmyron
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.
Re: Logic Life Search
Posted: July 17th, 2019, 6:16 pm
by LaundryPizza03
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
Re: Logic Life Search
Posted: July 18th, 2019, 1:56 am
by LaundryPizza03
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?
Re: Logic Life Search
Posted: July 18th, 2019, 6:14 am
by wildmyron
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.
Re: Logic Life Search
Posted: July 19th, 2019, 3:27 pm
by LaundryPizza03
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.
Re: Logic Life Search
Posted: July 20th, 2019, 4:47 pm
by LaundryPizza03
Thanks, it helped me find a 29c/29o and a (6,5)c/18 much faster.
Re: Logic Life Search
Posted: September 5th, 2019, 6:50 pm
by AlephAlpha
Could you add an option to force the first row/column to be nonempty? That might be helpful for long and thin patterns.
Re: Logic Life Search
Posted: November 23rd, 2019, 8:32 pm
by Scorbie
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?
Re: Logic Life Search
Posted: November 26th, 2019, 8:56 pm
by Scorbie
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.
Re: Logic Life Search
Posted: February 20th, 2020, 8:11 pm
by LaundryPizza03
I have a question.
When I copy-paste this file:
Code: Select all
0' 0 0 0 0 0 0 0 0
0' 0 0 0 0 1 0 0 0
0' 0 1 1 1 1 1 0 0
0' 0 0 1 1 0 1 0 0
0' a1 a2 a3 a4 a5 a6 a7 0
*' b1 b2 b3 b4 b5 b6 b7 0
*' c1 c2 c3 c4 c5 c6 c7 0
*' *' *' *' *' *' *' *' *'
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
*' * * * * * * * *
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
*' * * * * * * * *
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
*' * * * * * * * *
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
0' 0 0 0 0 0 1 0 0
0' 0 0 1 1 1 1 1 0
0' 0 0 0 1 1 0 1 0
0' * a1 a2 a3 a4 a5 a6 a7
0' * b1 b2 b3 b4 b5 b6 b7
*' * c1 c2 c3 c4 c5 c6 c7
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
the last phase is copied improperly and LLS crashes as non-cuboidal. But if I copy it piece-by-piece to avoid this, it still crashes.
Re: Logic Life Search
Posted: February 21st, 2020, 4:54 am
by Macbi
Try replacing the double spaces with single spaces. (Or if you want everything to remain beautifully aligned then replace the single spaces with commas and the double spaces with commas followed by a space.)
Re: Logic Life Search
Posted: February 28th, 2020, 5:49 am
by LaundryPizza03
Macbi wrote: February 21st, 2020, 4:54 am
LaundryPizza03 wrote: February 20th, 2020, 8:11 pm
I have a question.
When I copy-paste this file:
Code: Select all
0' 0 0 0 0 0 0 0 0
0' 0 0 0 0 1 0 0 0
0' 0 1 1 1 1 1 0 0
0' 0 0 1 1 0 1 0 0
0' a1 a2 a3 a4 a5 a6 a7 0
*' b1 b2 b3 b4 b5 b6 b7 0
*' c1 c2 c3 c4 c5 c6 c7 0
*' *' *' *' *' *' *' *' *'
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
*' * * * * * * * *
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
*' * * * * * * * *
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
0' * * * * * * * *
*' * * * * * * * *
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
0' 0 0 0 0 0 1 0 0
0' 0 0 1 1 1 1 1 0
0' 0 0 0 1 1 0 1 0
0' * a1 a2 a3 a4 a5 a6 a7
0' * b1 b2 b3 b4 b5 b6 b7
*' * c1 c2 c3 c4 c5 c6 c7
*' * * * * * * * *
*' *' *' *' *' *' *' *' *'
the last phase is copied improperly and LLS crashes as non-cuboidal. But if I copy it piece-by-piece to avoid this, it still crashes.
Try replacing the double spaces with single spaces. (Or if you want everything to remain beautifully aligned then replace the single spaces with commas and the double spaces with commas followed by a space.)
It still crashes.
Code: Select all
0' 0 0 0 0 0 0 0 0 0 0 0'
0' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 0'
0' b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 0'
0' c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 0'
0' m0' m1' m2' m3' m4' m5' m6' m7' m8' m9' 0'
0' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 0'
0' y0 y1 y2 y3 y4 y5 y6 y7 y8 y9 0'
0' z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 0'
0' 0 0 0 0 0 0 0 0 0 0 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' n0' n1' n2' n3' n4' n5' n6' n7' n8' n9' 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' m0' m1' m2' m3' m4' m5' m6' m7' m8' m9' 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' n0' n1' n2' n3' n4' n5' n6' n7' n8' n9' 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' m0' m1' m2' m3' m4' m5' m6' m7' m8' m9' 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' n0' n1' n2' n3' n4' n5' n6' n7' n8' n9' 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' m0' m1' m2' m3' m4' m5' m6' m7' m8' m9' 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' * * * * * * * * * * 0'
0' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 0'
0' b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 0'
0' c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 0'
0' * * * * * * * * * * 0'
0' m0' m1' m2' m3' m4' m5' m6' m7' m8' m9' 0'
0' y0 y1 y2 y3 y4 y5 y6 y7 y8 y9 0'
0' z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 0'
0' 0 0 0 0 0 0 0 0 0 0 0'
0' 0 0 0 0 0 0 0 0 0 0 0'
Re: Logic Life Search
Posted: February 28th, 2020, 6:47 am
by Macbi
Try adding an extra newline at the end.
Re: Logic Life Search
Posted: July 9th, 2020, 11:09 pm
by Hunting
When I try the test pattern in the OP, this is what happens:
Code: Select all
root@LD:/mnt/c/Users/Administrator/logic-life-search# ./lls test.txt -S lingeling -i
Getting search pattern...
Done
Preprocessing...
Done
Number of undetermined cells: 0
Number of variables: 0
Number of clauses: 1
Active width: 0
Active height: 0
Active duration: 0
Solving...
Done
Time taken: 0.0034818649292 seconds
Unsatisfiable
Re: Logic Life Search
Posted: July 10th, 2020, 2:36 am
by wildmyron
Hunting wrote: July 9th, 2020, 11:09 pm
When I try the test pattern in the OP, this is what happens:
Code: Select all
root@LD:/mnt/c/Users/Administrator/logic-life-search# ./lls test.txt -S lingeling -i
Getting search pattern...
Done
Preprocessing...
Done
Number of undetermined cells: 0
Number of variables: 0
Number of clauses: 1
Active width: 0
Active height: 0
Active duration: 0
Solving...
Done
Time taken: 0.0034818649292 seconds
Unsatisfiable
That is very strange output. There seems to be a very constrained pattern in your text file. After some mucking about I found the following search pattern produces the same result:
Does the following command give the expected output (should be the search pattern)? [ If it looks like it does, then please copy and paste the output here. ]
Or if you put test.txt in search_patterns directory:
Re: Logic Life Search
Posted: July 10th, 2020, 4:18 am
by Saka
I noticed that in the OP cells are separated by spaces but in LLS they should be separated by commas (",") (this is the case in the development version, but I think it is the same in the "master" version). Try replacing all the spaces with commas?
Re: Logic Life Search
Posted: July 10th, 2020, 7:13 am
by Macbi
Saka wrote: July 10th, 2020, 4:18 am
I noticed that in the OP cells are separated by spaces but in LLS they should be separated by commas (",") (this is the case in the development version, but I think it is the same in the "master" version). Try replacing all the spaces with commas?
LLS can handle both commas and spaces.
I think the problem is in test.txt. Possibly it has something to do with how Windows treats newlines differently from Linux. Can you try again using this file?
Re: Logic Life Search
Posted: July 10th, 2020, 7:19 am
by Saka
Mac​bi wrote: July 10th, 2020, 7:13 am
LLS can handle both commas and spaces.
Well that's embarrassing, oops
Re: Logic Life Search
Posted: July 10th, 2020, 12:24 pm
by wildmyron
Macbi wrote: July 10th, 2020, 7:13 am
I think the problem is in test.txt. Possibly it has something to do with how Windows treats newlines differently from Linux. Can you try again using this file? test2.txt
Yes, that seems quite likely. The following search pattern causes the same output:
I'm a bit surprised that LLS doesn't find that to be UNSAT in pre-processing on account of the first generation being all '0' combined with '-i' (or '-p ">2"', as the case may be).
Re: Logic Life Search
Posted: August 4th, 2020, 4:13 pm
by LaundryPizza03
I can't submit custom inputs using STDIN for some reason; I can use them only as files. Where does the EOF character go?
Code: Select all
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
a11 a12 a13 0 0 b11 b12 b13 0 0
a21 a22 a23 0 0 b21 b22 b23 0 0
0 0 0 0 0 b31 b32 b33 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 a11 a12 a13 0 b11 b12 b13 0 0
0 a21 a22 a23 0 b21 b22 b23 0 0
0 0 0 0 0 b31 b32 b33 0 0
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
* * * * * * * * * *
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 a21 a11 0 0 0
0 0 0 0 0 a22 a12 0 0 0
0 0 0 0 0 a23 a13 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0
Re: Logic Life Search
Posted: August 5th, 2020, 12:34 am
by wildmyron
LaundryPizza03 wrote: August 4th, 2020, 4:13 pm
I can't submit custom inputs using STDIN for some reason; I can use them only as files. Where does the EOF character go?
Are you getting stdin by redirecting from a file or by pasting to the console? If the former then the EOL char comes from the file. If the latter then the EOL char can be provided by typing Ctrl-D after pasting.
If that doesn't help resolve the issue then please provide more details about how you are invoking LLS and what steps you are carrying out.