ConwayLife.com

Posted: **December 4th, 2018, 8:03 pm**

Does anyone know how to fix this error? It says "[Errno 13] Permission denied", and I'm pretty sure I did everything else correctly: I installed all the necessary packages, I installed Lingeling, extracted it, configured it, and put the folder inside the solvers directory. I'm also running Cygwin as an administrator.

Code: Select all

Traceback (most recent call last):
  File "./lls", line 195, in <module>
    indent = indent, verbosity = verbosity
  File "/home/ionma/logic-life-search/src/LLS.py", line 61, in preprocess_solve_and_postprocess
    indent = indent, verbosity = verbosity
  File "/home/ionma/logic-life-search/src/LLS.py", line 175, in preprocess_and_solve
    indent = indent, verbosity = verbosity)
  File "/home/ionma/logic-life-search/src/LLS.py", line 246, in solve
    DIMACS_string, solver=solver, parameters=parameters, timeout=timeout, save_dimacs = save_dimacs, dry_run = dry_run, indent = indent + 1, verbosity = verbosity)
  File "/home/ionma/logic-life-search/src/LLS_SAT_solvers.py", line 48, in SAT_solve
    solution, time_taken = use_solver(solver, dimacs_file, parameters = parameters, timeout = timeout, indent = indent, verbosity = verbosity)
  File "/home/ionma/logic-life-search/src/LLS_SAT_solvers.py", line 86, in use_solver
    stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
  File "/usr/lib/python2.7/subprocess.py", line 390, in __init__
    errread, errwrite)
  File "/usr/lib/python2.7/subprocess.py", line 1025, in _execute_child
    raise child_exception
OSError: [Errno 13] Permission denied

EDIT: I've now tried putting the application itself in the solvers folder on its own and it still gives the exact same error.

I've also tried setting the solver to lingeling.exe instead of just lingeling, which just says it can't find the solver:

Code: Select all

Traceback (most recent call last):
  File "./lls", line 195, in <module>
    indent = indent, verbosity = verbosity
  File "/home/ionma/logic-life-search/src/LLS.py", line 61, in preprocess_solve_and_postprocess
    indent = indent, verbosity = verbosity
  File "/home/ionma/logic-life-search/src/LLS.py", line 175, in preprocess_and_solve
    indent = indent, verbosity = verbosity)
  File "/home/ionma/logic-life-search/src/LLS.py", line 246, in solve
    DIMACS_string, solver=solver, parameters=parameters, timeout=timeout, save_dimacs = save_dimacs, dry_run = dry_run, indent = indent + 1, verbosity = verbosity)
  File "/home/ionma/logic-life-search/src/LLS_SAT_solvers.py", line 32, in SAT_solve
    assert solver in solvers, "Solver not found"
AssertionError: Solver not found

Same deal for plingeling and treengeling.

Posted: **December 4th, 2018, 8:27 pm**

Ian07 wrote:Does anyone know how to fix this error? It says "[Errno 13] Permission denied", and I'm pretty sure I did everything else correctly: I installed all the necessary packages, I installed Lingeling, extracted it, configured it, and put the folder inside the solvers directory. I'm also running Cygwin as an administrator.
Code: Select all
[...]

The problem is occurring when LLS tries to call Lingeling. LLS doesn't yet have permission to do this. I don't use Windows or Cygwin but I imagine the solution is something like the following

Right click on Lingeling
Go to "Properties"
Go to something like "Permissions" or "Security"
Allow Lingeling to excecute

I don't think you should have to be Administrator for LLS to work (you might have to be Administrator to change the permissions?). You're running LLS so as long as you yourself have permission to run Lingeling it should work fine.

Posted: **December 4th, 2018, 8:59 pm**

Macbi wrote: The problem is occurring when LLS tries to call Lingeling. LLS doesn't yet have permission to do this. I don't use Windows or Cygwin but I imagine the solution is something like the following
Right click on Lingeling
Go to "Properties"
Go to something like "Permissions" or "Security"
Allow Lingeling to excecute
I don't think you should have to be Administrator for LLS to work (you might have to be Administrator to change the permissions?). You're running LLS so as long as you yourself have permission to run Lingeling it should work fine.

Hmm, according to the security panel I should already have full permissions for lingeling.exe

When I tried to run Lingeling directly to see what would happen, an error popped up saying:

Code: Select all

The code execution cannot proceed because cygwin1.dll was not found. Reinstalling the program may fix this problem.

...even though I definitely already have the DLL in my Cygwin bin.

Posted: **December 4th, 2018, 9:06 pm**

Okay, well it looks like the problem is with Lingeling and Cygwin rather than with LLS. Sorry I can't help you more.

EDIT: A quick Google suggests that the problem might be that Cygwin isn't in your PATH variable.

Posted: **December 5th, 2018, 12:49 am**

If Macbi's suggestion of checking cygwin's PATH variable doesn't solve your problem and you still can't get LLS to run, then you might like to try using LLS with the glucose binary I posted earlier in the thread. You don't need cygwin at all then, but you may wish to use it for Bash and the nicer console. Previously I used the console and Bash provided by MSYS (bundled with the mingw-w64 project) but since I moved to Win10 I've been using Ubuntu under Windows Subsystem for Linux which makes a lot of these cross platform compatibility issues a lot easier to deal with.

If you're not already, I'd also advise to switch to the develop branch on the LLS repository. @Macbi: Seeing as there's been a pause in development of LLS, it would be great if you could merge that branch with master.

Posted: **December 5th, 2018, 5:35 pm**

wildmyron wrote:If Macbi's suggestion of checking cygwin's PATH variable doesn't solve your problem and you still can't get LLS to run, then you might like to try using LLS with the glucose binary I posted earlier in the thread. You don't need cygwin at all then, but you may wish to use it for Bash and the nicer console. Previously I used the console and Bash provided by MSYS (bundled with the mingw-w64 project) but since I moved to Win10 I've been using Ubuntu under Windows Subsystem for Linux which makes a lot of these cross platform compatibility issues a lot easier to deal with.

It worked, thanks!

Code: Select all

$ ./lls -S glucose-syrup -m -b 16 6 -p 3 -x 0 -y 1

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 272
Number of variables: 416
Number of clauses: 36467

Active width: 16
Active height: 6
Active duration: 4

Solving...
Done

Time taken: 0.429523229599 seconds

x = 18, y = 8, rule = B3/S23
bbbbbbbbbbbbbbbbbb$
bboobbbbbbbbbbbbbb$
bobbbbobbbobbboobb$
bboooobboobbbbbbob$
bbbbbooboboobooobb$
bbbbbbbboobobbbbbb$
bbbbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbbbb!

wildmyron wrote:If you're not already, I'd also advise to switch to the develop branch on the LLS repository.

Done.

Posted: **December 22nd, 2018, 12:18 pm**

Search for orphans (GoE's) does not seem to work.
**EDIT: found the solution, see at the bottom**

I run lls with the following command line

Code: Select all

./lls -S glucose -v 3 --check_orphan GoE1.txt

and the this output:

Code: Select all

Getting search pattern...
    Creating search pattern to see if file "GoE1.txt" contains an orphan...
        Reading file "GoE1.txt" ...
        Done

        Parsing input pattern...
        Done

        Pattern parsed as:
        *0100010**
        *101010110
        0100011001
        1010000010
        0110110000
        0000110110
        0100000101
        1001100010
        011010101*
        **0100010*



        Search pattern:
        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'

    Done

    Standardising variable names...
    Done

Done

Preprocessing...
    Preparing search grid ...
    Done

    Enforcing evolution rule...
        Method: 1
        Number of clauses used: 0
    Done

    Converting to DIMACS format...
    Done

Number of undetermined cells: 0
Number of variables: 0
Number of clauses: 0

Active width: 0
Active height: 0
Active duration: 0

Solving...
    Preparing SAT solver input...
        Writing file "lls_dimacs3.cnf" ...
        Done

    Done

    Solving with "glucose" ... (Start time: Sat Dec 22 18:09:16 2018)
    Done

    Formatting SAT solver output...
        SAT solver output:
            c
            c This is glucose 4.0 --  based on MiniSAT (Many thanks to MiniSAT team)
            c
            c ========================================[ Problem Statistics ]===========================================
            c |                                                                                                       |
            c |  Number of variables:             0                                                                   |
            c |  Number of clauses:               0                                                                   |
            c |  Parse time:                   0.00 s                                                                 |
            c |                                                                                                       |
            c | Preprocesing is fully done
            c |  Simplification time:          0.00 s                                                                 |
            c |                                                                                                       |
            c ========================================[ MAGIC CONSTANTS ]==============================================
            c | Constants are supposed to work well together :-)                                                      |
            c | however, if you find better choices, please let us known...                                           |
            c |-------------------------------------------------------------------------------------------------------|
            c | Adapt dynamically the solver after 100000 conflicts (restarts, reduction strategies...)               |
            c |-------------------------------------------------------------------------------------------------------|
            c |                                |                                |                                     |
            c | - Restarts:                    | - Reduce Clause DB:            | - Minimize Asserting:               |
            c |   * LBD Queue    :     50      |   * First     :   2000         |    * size <  30                     |
            c |   * Trail  Queue :   5000      |   * Inc       :    300         |    * lbd  <   6                     |
            c |   * K            :   0.80      |   * Special   :   1000         |                                     |
            c |   * R            :   1.40      |   * Protected :  (lbd)< 30     |                                     |
            c |                                |                                |                                     |
            c ==================================[ Search Statistics (every  10000 conflicts) ]=========================
            c |                                                                                                       |
            c |          RESTARTS           |          ORIGINAL         |              LEARNT              | Progress |
            c |       NB   Blocked  Avg Cfc |    Vars  Clauses Literals |   Red   Learnts    LBD2  Removed |          |
            c =========================================================================================================
            c last restart ## conflicts  :  0 0
            c =========================================================================================================
            c restarts              : 1 (0 conflicts in avg)
            c blocked restarts      : 0 (multiple: 0)
            c last block at restart : 0
            c nb ReduceDB           : 0
            c nb removed Clauses    : 0
            c nb learnts DL2        : 0
            c nb learnts size 2     : 0
            c nb learnts size 1     : 0
            c conflicts             : 0              (-nan /sec)
            c decisions             : 1              (0.00 % random) (inf /sec)
            c propagations          : 0              (-nan /sec)
            c nb reduced Clauses    : 0
            c CPU time              : 0 s

            s SATISFIABLE
            v  0

        Error (if any): ""
        Time taken: 0.00165295600891
    Done

    Removing DIMACS file...
    Done

    Substituting solution back into search grid...
    Done

Done

Time taken: 0.00165295600891 seconds

Formatting output...
    Format: RLE
Done

x = 3, y = 12, rule = B3/S23
bbb$
bbb$
bbb$
bbb$
bbb$
bbb$
bbb$
bbb$
bbb$
bbb$
bbb$
bbb!

Obviously lls is not translating the input pattern correctly. How do I fix this?

EDIT
Never mind, found it.
The solution is to put comma's in the input file, like so

Code: Select all

*,*,1,0,1,0,1.....
.....

Posted: **December 23rd, 2018, 3:58 am**

Right, anything not separated by commas or spaces is just a very long variable name.

Posted: **June 22nd, 2019, 12:55 am**

I cloned LLS into a directory and attempted to run it from the command line. It demands some "/usr" directory that doesn't exist. What do I do?

Code: Select all

[my]-iMac:logic-life-search [user]$ ./lls -S lingeling -m -b 16 6 -p 3 -x 0 -y 1
-bash: ./lls: /usr/bin/python2: bad interpreter: No such file or directory

I am running in Mac OS 10.14.2.

Posted: **June 22nd, 2019, 4:13 am**

LaundryPizza03 wrote:I cloned LLS into a directory and attempted to run it from the command line. It demands some "/usr" directory that doesn't exist. What do I do?
Code: Select all
[my]-iMac:logic-life-search [user]$ ./lls -S lingeling -m -b 16 6 -p 3 -x 0 -y 1
-bash: ./lls: /usr/bin/python2: bad interpreter: No such file or directory
I am running in Mac OS 10.14.2.

If you open lls in a text editor you'll see that the first line contains "/usr/bin/python2". You need to edit this to instead be wherever python2 lives on your machine. You should be able to find this out using one of the suggestions on this thread: https://stackoverflow.com/questions/676 ... efault-dir.

Alternatively you should be able to just run

Code: Select all

python2 lls -S lingeling -m -b 16 6 -p 3 -x 0 -y 1

Posted: **June 22nd, 2019, 7:25 am**

How do I eliminate subperiods, like you did in this post? I know that forcing a different number of cells after one subperiod will work, for obvious reasons, but this might not allow the full range of solutions.

Posted: **June 22nd, 2019, 7:47 am**

Umm.. first of all you're using an outdated version of LLS. Use the "development" branch instead.

To enforce the symmetry of a period, use "-s p7" or "-s p11" or "-s p(period)".
To enforce the ASYMMETRY of a period (i.e. NOT this period), use "-a p1" or "-a p(a divisor of the period)". Normally "-a p1" is required for most searches.

The wiki's outdated

Posted: **June 22nd, 2019, 11:52 am**

testitemqlstudop wrote:The wiki's outdated

If only there were a way to edit it...!

Posted: **June 22nd, 2019, 5:13 pm**

testitemqlstudop wrote:Umm.. first of all you're using an outdated version of LLS. Use the "development" branch instead.

To enforce the symmetry of a period, use "-s p7" or "-s p11" or "-s p(period)".
To enforce the ASYMMETRY of a period (i.e. NOT this period), use "-a p1" or "-a p(a divisor of the period)". Normally "-a p1" is required for most searches.

The wiki's outdated

Okay, so how do I find a spaceship with a particular displacement? The develop branch doesn't have such an option.

Posted: **June 22nd, 2019, 9:17 pm**

LaundryPizza03 wrote:Okay, so how do I find a spaceship with a particular displacement? The develop branch doesn't have such an option.

The displacement and glide reflection of a spaceship can be specified as part of the symmetry option. So to find a 2c/4 ship with glide reflection you can do:

Code: Select all

./lls -p ">1" -s p4 "RE-" x2 -a p2 x1 -b [X] [Y]

and to find a 2c/4 ship with bilateral symmetry you can do:

Code: Select all

./lls -p ">1" -s p4 x2 -s "D2-" -a p2 x1 -b [X] [Y]

In both cases the '-a p2 x1' option excludes c/2 ships with bilateral symmetry which would otherwise be valid solutions and '-p ">1"' enforces a non-empty ship (although not necessary when forcing an asymmetry as that would also exclude those solutions".

@Macbi: When I try to use the notation in the help, e.g. '-s "p4 RE- x2"' I get an error:

Code: Select all

Getting search pattern...
Traceback (most recent call last):
  File "./lls", line 327, in <module>
    assert transformation in ["RE-","RE/","RE|","RE\\"], 'Symmetry argument "' + transformation + '" not recognized'
AssertionError: Symmetry argument "P4 X2 RE-" not recognized

Posted: **June 23rd, 2019, 3:39 am**

wildmyron wrote:@Macbi: When I try to use the notation in the help, e.g. '-s "p4 RE- x2"' I get an error:
Code: Select all
Getting search pattern...
Traceback (most recent call last):
  File "./lls", line 327, in <module>
    assert transformation in ["RE-","RE/","RE|","RE\\"], 'Symmetry argument "' + transformation + '" not recognized'
AssertionError: Symmetry argument "P4 X2 RE-" not recognized

LLS is getting "p4 RE- x2" all as one argument, when it wants three distinct arguments. Simply removing the quotes fixes it for me:

Code: Select all

$ ./lls -b11 -s p4 RE- x2 -c

Getting search pattern...
Done

Preprocessing...
Done

Number of undetermined cells: 451
Number of variables: 562
Number of clauses: 62374

Active width: 11
Active height: 11
Active duration: 5

Solving...
Done

Time taken: 0.86586022377 seconds

x = 13, y = 13, rule = B3/S23
bbbbbbbbbbbbb$
bbbbbbbbbbbbb$
bbbbbbboobbbb$
bbbbbooboobbb$
bbbbboooobbbb$
bbbbbboobbbbb$
bbbbbbbbbbbbb$
bbbbbboobbbbb$
bbbbboooobbbb$
bbbbbooboobbb$
bbbbbbboobbbb$
bbbbbbbbbbbbb$
bbbbbbbbbbbbb!

Posted: **July 12th, 2019, 5:55 pm**

Here’s something curious about the asymmetry tag. When I ran

Code: Select all

./lls -S lingeling -b 14 8 -s p14 x10 y4 -p "<=5" -a p7 -r pB2ac3-i45678/S012345678

to find a (10,4)c/14 for 5s, I eventually got

Code: Select all

x = 16, y = 10, rule = B2-en3jnqr4ekrwyz5aeq6-a7/S01e2e3-cijn4-aceiwz5-anqy6e8
bbbbbbbbbbbbbbbb$
bbbbobbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bobbbbbbbbbbbbbb$
bbooobbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb!

, which, as you can verify for yourself, is a (5,2)c/7.
However,

Code: Select all

./lls -S lingeling -b 14 8 -s p14 x10 y4 -p "<=5" -a p7 x5 y2 -r pB2ac3-i45678/S012345678

returns the expected result, since it says that the pattern must not be a (5,2)c/7. I eventually found

Code: Select all

x = 16, y = 10, rule = B2ac3ar4-qtyz5akny6aik7c/S1e2n3aeiry4-jnqwy5ejqr6k7e
bbbbbbbbbbbbbbbb$
bbbbobbbbbbbbbbb$
bbobbbbbbbbbbbbb$
bbbbobbbbbbbbbbb$
bbobobbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb!

, which is indeed a (10,4)c/14.

Posted: **July 13th, 2019, 1:15 am**

In the final CNF file, how should I go mapping (x, y, t) triplets to variable IDs?

Posted: **July 13th, 2019, 1:57 am**

LaundryPizza03 wrote:Here’s something curious about the asymmetry tag. When I ran
Code: Select all
./lls -S lingeling -b 14 8 -s p14 x10 y4 -p "<=5" -a p7 -r pB2ac3-i45678/S012345678
to find a (10,4)c/14 for 5s, I eventually got
Code: Select all
x = 16, y = 10, rule = B2-en3jnqr4ekrwyz5aeq6-a7/S01e2e3-cijn4-aceiwz5-anqy6e8
bbbbbbbbbbbbbbbb$
bbbbobbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bobbbbbbbbbbbbbb$
bbooobbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb$
bbbbbbbbbbbbbbbb!
, which, as you can verify for yourself, is a (5,2)c/7

This is expected behaviour. The asymmetry you specified is equivalent to "-a p7 x0 y0", which forbids a p7 oscillator.

testitemqlstudop wrote:In the final CNF file, how should I go mapping (x, y, t) triplets to variable IDs?

I can't remember where this is explained in this thread, but here's a relevant extract from my notes about this.

Code: Select all

# Use lls to generate a cnf file and save the search state (for later solution substitution)

$ python lls partial.txt -r pB2ac345678S012345678 -s "D2-" --optimise --dry_run --save_state partial.pkl --save_dimacs partial.cnf

# Check the correspondence between grid cells and cnf variables

$ python -i
>>> import pickle
>>> from src.SearchPattern import SearchPattern
>>> (grid, ignore_transition, rule, correspondence) = pickle.load(open("partial.pkl","r"))
>>> search_pattern = SearchPattern(grid)
>>> print search_pattern.make_string(pattern_output_format = "csv")

# Find the grid cells of interest and determine the variables corresponding to those grid cells

>>> [int(correspondence[v]) for  v in ["c615","c626","c637","c648","c659","c670","c681","c692","c703","c714","c725"]]
>>> quit()

# Run the SAT solver. If a solution is found, copy the last two lines of output (starting with s and v) to a file: partial.soln
$ ./solvers/glucose-syrup partial.cnf -model

# Substitute the solution back in to the grid with lls
$ python lls --substitute_solution partial.pkl partial.soln

Edit: oops, I snipped the important step, now added back into the instructions. I've left out the other details related to partials as that's not relevant here

Posted: **July 13th, 2019, 6:17 am**

I updated the notes relating to grid cell <--> variable correspondence as I had left out a vital instruction.

Posted: **July 13th, 2019, 9:00 am**

I get this:

Code: Select all

>>> (grid, ignore_transition, rule, correspondence) = pickle.load(open("p4ph.pkl","r"))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ValueError: too many values to unpack
>>> (grid, rule, correspondence) = pickle.load(open("p4ph.pkl","r"))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ValueError: too many values to unpack
>>> (grid, correspondence) = pickle.load(open("p4ph.pkl","r"))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ValueError: too many values to unpack
>>> len(pickle.load(open("p4ph.pkl","r")))
6
>>>

I called

Code: Select all

./lls -s p4 -a p1 -a p2 -b 15 --dry_run --save_state p4ph.pkl --save_dimacs p4ph.cnf

Posted: **July 13th, 2019, 9:28 am**

testitemqlstudop wrote:I get this:

Code: Select all

>>> (grid, ignore_transition, rule, correspondence) = pickle.load(open("p4ph.pkl","r"))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ValueError: too many values to unpack
<snip>

I presume that means the objects saved to the pickle file have changed since I wrote those notes. Looking at the code for --save-state it looks like you should do this instead:

Code: Select all

>>> (grid, _, _, _, rule, correspondence) = pickle.load(open("partial.pkl","r"))

You don't need ignore_transition, and the two additional objects are background_grid and background_ignore_transition - required for lls' support for non vacuum backgrounds.

Posted: **July 13th, 2019, 9:58 pm**

It works now, thanks!

Posted: **July 16th, 2019, 12:06 am**

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?

Posted: **July 16th, 2019, 2:18 am**

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.

ConwayLife.com

Logic Life Search (LLS)

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search

Re: Logic Life Search