Comments

[yoni206]

1. Please include at the top of the readme a link to the web thingy.
2. The repo is too big. Please compress all the benchmarks and raw results, and also provide lesser quality pictures. Don't compress the examples though.
3. Please soft-wrap this Readme, so that each line does not have more than 80 characters. This will make it easier to make comments on specific parts.
4. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L3 "pysmt and cvc5 solvers" -> "pysmt and cvc5".
5. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L5 "and and"
6. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L8 better be "Implemented Reductions -- Theories and Solvers"
7. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L23 Y -> y
8. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L63 Please provide code examples for how to run this. Also show and explain the output. This part of the Readme is very important, as it is where you show how to use the tool.
9. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L63 This actually doesn't work for me on ubuntu... I get

   panda@panda:~/git/k-coloringReduction$ python3 Examples/examplePySMT.py
   /home/panda/.local/lib/python3.10/site-packages/pysmt/smtlib/parser/__init__.py:83: DeprecationWarning: the imp module is deprecated in favour of importlib and slated for removal in Python 3.12; see the module's documentation for alternative uses
   import imp
   Traceback (most recent call last):
   File "/home/panda/git/k-coloringReduction/Examples/examplePySMT.py", line 9, in <module>
   from Reduction import reduction
   File "/home/panda/git/k-coloringReduction/Reduction/reduction.py", line 2, in <module>
   from pysmt.shortcuts import Solver as pysmt_solver
   File "/home/panda/.local/lib/python3.10/site-packages/pysmt/shortcuts.py", line 38, in <module>
   import pysmt.smtlib.parser
   File "/home/panda/.local/lib/python3.10/site-packages/pysmt/smtlib/parser/__init__.py", line 91, in <module>
   so_path = pyximport.build_module(name, path,
   AttributeError: module 'pyximport' has no attribute 'build_module'

   I think that the fastest way forward to fix this is to use docker and provide a docker image. That way, no matter on what machine people run it, it will work.

10. Please include a link for DIMACS COLOR02.30.04 challenge and may say a few words about it.
11. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L75 This is not very clear. Please try to provide more details and be more clear about the precise results.
12. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L81 "sometimes ordered by theory" doesn't sound good... Why sometimes?
13. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L82 Maybe "As" should be "We"?
14. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L100 it is unclear what does "the result is 16" mean.
15. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L104 "DDespite" -> "Despite". Also english-wise it doesn't sound right.
16. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L104 "performed better" -- better than what?
17. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L104 "The source image is available in the files" -- please provide a path/link.
18. https://github.com/guretskiysemyon/k-coloringReduction/blob/eb8296f9ecf05f3569d0c28df080cf062f0ae056/readme.md?plain=1#L109 Why did you seperate BV and Sets from the rest? Either merge or explain in the text. Also: "The results are the same" is unclear.
19. At the end please add a conclusion section, that summarizes the work, describes the main results, challenges you faced, and what can be done next in this context.

[guretskiysemyon]

Tnank you for feedback! I changed the points to numbers in your comment for more comfortable references.

1. Done
2. Changed the resolution of the images. I still wanted them to be readable, so the size became smaller by 2 or 5 times. Let me know if it still doesn't look good; maybe I'll add additional images in lesser quality only for the readme. The benchmarks and results CSV files are also compressed to the size that git allows.
3. Done. 4, 5, 6, 7, 12, 13, 15: All mistakes in words and English corrected in the way you suggested.
4. Removed those files and changed the reduction folder so that it can be called from the CLI. I did this to make it possible to run Docker without using any additional files, and to make it easy to use the tool without needing to write code. Files will be available for development purposes in the repository. Following your recommendation, I added output. I tried to make it more readable in the CLI and added color to the output in the terminal. I hope this is sufficient. If you think there needs to be more information, please let me know and I'll try to improve it.
5. It took me a while because of btor; I had some installation problems again. I created a Docker image that I placed in Docker Hub. I wrote the command to pull it and how to run it. I didn't explain how to mount or copy data to Docker, assuming that this is accessible information. There is a small issue: on the first reduction tool run, it compiles some files and it takes about 20 seconds, but all subsequent queries work normally.
6. Added a link and a small explanation from their site. 11, 14, 16, 18: Tried to improve readability and explain. Let me know if it's still not clear.
7. Added path.
8. There were a conclusion and future work section, but I changed them a bit. Added more ideas. Hope this is what you meant.

[yoni206]

Thanks. It is ok if docker takes time in the first time, as long as you mention it. But, let's assume 0 familiarity with docker. So either put the command to mount, or (maybe easier) copy the files into the docker image. Once something like that is done, I can actually check if it works locally.

python3 reduction Benchmarks/graph.dot 3 z3 LIA --t-10

This doesn't look right. reduction is a directory, not a python script. Also here:

python3 reduction <path-to-dot-file> <number-of-colors> <solver-name> <theory-name>

[guretskiysemyon]

• I have added more information about Docker. I explained that the first command creates the container, provided details on how to choose a name, and how to run the container next time using that name. I also included an explanation on how to mount files to the Docker container.
• I have added a main.py file to the folder, so Python should recognize it and run the program from there. I thought this might be more convenient than having to type reduction/reduction.py. It worked for me and for a few people I asked to check it. Let me know if you encounter any issues, and I will check.

[yoni206]

Still doesn't work for me with several issues... Please try to make the docker instructions more accurate and detailed. Also please consider use the COPY command in the Dockerfile to just copy all the graph files into the image.

On Mon, Oct 14, 2024 at 12:41 PM Semyon Guretskiy @.***> wrote:

• I have added more information about Docker. I explained that the first command creates the container, provided details on how to choose a name, and how to run the container next time using that name. I also included an explanation on how to mount files to the Docker container.
• I have added a main.py file to the folder, so Python should recognize it and run the program from there. I thought this might be more convenient than having to type reduction/reduction.py. It worked for me and for a few people I asked to check it. Let me know if you encounter any issues, and I will check.

— Reply to this email directly, view it on GitHub https://github.com/guretskiysemyon/k-coloringReduction/issues/2#issuecomment-2410615959, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADAKGREBISTGSJKTW3JO7YLZ3OGVZAVCNFSM6AAAAABPT2YBB2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMJQGYYTKOJVHE . You are receiving this because you authored the thread.Message ID: @.***>

[guretskiysemyon]

I am concerned that adding all the files to the container might significantly increase its size. However, I can do it if necessary. Could you provide your output so I can understand at which step it fails and identify what the problem could be? Is the issue only with the mounting step?

[yoni206]

First, please avoid from providing both the command without the mount and the command without the mount, as the first creates something that the second asks to step on... So just directly give in the Readme the command with the mount (including examples).

Now, I managed to get it to work but:

1. If you are already mounting, why mounting only a single file and not the entire directory?
2. Can you make sure some editor like vi or something is included in the docker image so that files can be edited?

On Mon, Oct 14, 2024 at 2:17 PM Semyon Guretskiy @.***> wrote:

I am concerned that adding all the files to the container might significantly increase its size. However, I can do it if necessary. Could you provide your output so I can understand at which step it fails and identify what the problem could be? Is the issue only with the mounting step?

— Reply to this email directly, view it on GitHub https://github.com/guretskiysemyon/k-coloringReduction/issues/2#issuecomment-2410907272, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADAKGRCUETS7MGAQYH6DKYTZ3OR5VAVCNFSM6AAAAABPT2YBB2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMJQHEYDOMRXGI . You are receiving this because you authored the thread.Message ID: @.***>

[guretskiysemyon]

I understand now, you are right. I thought about providing short instructions for people familiar with Docker, and more detailed ones for those who aren't. However, you're right that this could be misleading. I've corrected it.

1. I mounted only the file as an example, to let people check if the tool works. I compressed the entire DOT folder to reduce the repository size. It can be unzipped and mounted. I can try adding an unzip command to Docker and update the command to mount all the zipped files in Docker, instead of mounting just the graph .dot file. Alternatively, I can add a note that the DOT folder with the benchmarks needs to be unzipped, and update the mounting command to be

docker run -it --name color-reduction -v <path-to-unziped-files-folder>:/app/input_files semyonguretskiy/color-reduction:v1 bash

In general, aside from the benchmarks we provided, my intention was to let users choose the files they want to run with the tool, instead of linking it to specific inputs. This is one of the reasons I didn't copy the files into the Docker image. Should I change it? And if so, what do you think is the best way to do it?

2. I’ve added Vim and Nano. Are there any other tools you think might be needed?

I also added a reference to your site. Please correct me if it's the wrong one, or if you prefer another reference.

[yoni206]

OK thanks. I'll check this tomorrow, and if all goes well will send the report then!

On Mon, Oct 14, 2024 at 4:33 PM Semyon Guretskiy @.***> wrote:

I understand now, you are right. I thought about providing short instructions for people familiar with Docker, and more detailed ones for those who aren't. However, you're right that this could be misleading. I've corrected it.

1. I mounted only the file as an example, to let people check if the tool works. I compressed the entire DOT folder to reduce the repository size. It can be unzipped and mounted. I can try adding an unzip command to Docker and update the command to mount all the zipped files in Docker, instead of mounting just the graph .dot file. Alternatively, I can add a note that the DOT folder with the benchmarks needs to be unzipped, and update the mounting command to be

docker run -it --name color-reduction -v

:/app/input_files semyonguretskiy/color-reduction:v1 bash In general, aside from the benchmarks we provided, my intention was to let users choose the files they want to run with the tool, instead of linking it to specific inputs. This is one of the reasons I didn't copy the files into the Docker image. Should I change it? And if so, what do you think is the best way to do it? 3. I’ve added Vim and Nano. Are there any other tools you think might be needed? I also added a reference to your site. Please correct me if it's the wrong one, or if you prefer another reference. — Reply to this email directly, view it on GitHub , or unsubscribe . You are receiving this because you authored the thread.Message ID: ***@***.***>

[yoni206]

Sorry for the hold up but vim and nano don't work for me in the image... [image: image.png]

As for the files, I think it is better to copy them to the image. People can still use new files if they want. Not critical though.

On Mon, Oct 14, 2024 at 8:46 PM Yoni @.***> wrote:

OK thanks. I'll check this tomorrow, and if all goes well will send the report then!

On Mon, Oct 14, 2024 at 4:33 PM Semyon Guretskiy @.***> wrote:

I understand now, you are right. I thought about providing short instructions for people familiar with Docker, and more detailed ones for those who aren't. However, you're right that this could be misleading. I've corrected it.

1. I mounted only the file as an example, to let people check if the tool works. I compressed the entire DOT folder to reduce the repository size. It can be unzipped and mounted. I can try adding an unzip command to Docker and update the command to mount all the zipped files in Docker, instead of mounting just the graph .dot file. Alternatively, I can add a note that the DOT folder with the benchmarks needs to be unzipped, and update the mounting command to be

docker run -it --name color-reduction -v

:/app/input_files semyonguretskiy/color-reduction:v1 bash In general, aside from the benchmarks we provided, my intention was to let users choose the files they want to run with the tool, instead of linking it to specific inputs. This is one of the reasons I didn't copy the files into the Docker image. Should I change it? And if so, what do you think is the best way to do it? 3. I’ve added Vim and Nano. Are there any other tools you think might be needed? I also added a reference to your site. Please correct me if it's the wrong one, or if you prefer another reference. — Reply to this email directly, view it on GitHub , or unsubscribe . You are receiving this because you authored the thread.Message ID: ***@***.***>

[guretskiysemyon]

Unfortunately, I cannot see the image you sent.

I’ve copied the files to the Docker image as you requested and updated the README with a note explaining that users can create the image themselves if needed.

Regarding Vim and Nano, I rebuilt the image, ran it on my device, then pushed, pulled, and ran it again. It works fine on my end. I understand that this might not fully resolve the issue, but I suspect it could be a synchronization problem or something else unrelated to the image itself. Please try pulling the image again and let me know if the issue persists.

You might also want to remove any previous containers with the same name before creating the new one. If it still doesn't work, I'll look into other solutions. I will be glad to see the output though.

[yoni206]

OK Seems to work. I'll send the report today.

But please: the container now does not have a directory called Benchmarks, but instead it is called benchmarks (lower case b). Also, the example file graph.dot is missing from the container. Please fix the container and the Readme accordingly, so that they match, and that there is a simple example working.

Thanks,

Yoni

On Tue, Oct 15, 2024 at 7:59 PM Semyon Guretskiy @.***> wrote:

Unfortunately, I cannot see the image you sent.

I’ve copied the files to the Docker image as you requested and updated the README with a note explaining that users can create the image themselves if needed.

Regarding Vim and Nano, I rebuilt the image, ran it on my device, then pushed, pulled, and ran it again. It works fine on my end. I understand that this might not fully resolve the issue, but I suspect it could be a synchronization problem or something else unrelated to the image itself. Please try pulling the image again and let me know if the issue persists.

You might also want to remove any previous containers before running the new one. If it still doesn't work, I'll look into other solutions.

Sorry for the hold up but vim and nano don't work for me in the image... [image: image.png] As for the files, I think it is better to copy them to the image. People can still use new files if they want. Not critical though. … <#m4070678143827241220> On Mon, Oct 14, 2024 at 8:46 PM Yoni @.> wrote: OK thanks. I'll check this tomorrow, and if all goes well will send the report then! On Mon, Oct 14, 2024 at 4:33 PM Semyon Guretskiy @.> wrote: > I understand now, you are right. I thought about providing short > instructions for people familiar with Docker, and more detailed ones for > those who aren't. However, you're right that this could be misleading. I've > corrected it. >

1. I mounted only the file as an example, to let people check if the > tool works. I compressed the entire DOT folder to reduce the repository > size. It can be unzipped and mounted. I can try adding an unzip command to Docker and update the command to mount all the zipped files in Docker, > instead of mounting just the graph .dot file. Alternatively, I can add a > note that the DOT folder with the benchmarks needs to be unzipped, and > update the mounting command to be > > docker run -it --name color-reduction -v > :/app/input_files > semyonguretskiy/color-reduction:v1 bash > > In general, aside from the benchmarks we provided, my intention was to > let users choose the files they want to run with the tool, instead of > linking it to specific inputs. This is one of the reasons I didn't copy the > files into the Docker image. Should I change it? And if so, what do you > think is the best way to do it? > > 3. I’ve added Vim and Nano. Are there any other tools you think might > be needed? > > I also added a reference to your site. Please correct me if it's the > wrong one, or if you prefer another reference. > > — > Reply to this email directly, view it on GitHub <#2 (comment) https://github.com/guretskiysemyon/k-coloringReduction/issues/2#issuecomment-2411287669>, or unsubscribe > https://github.com/notifications/unsubscribe-auth/ADAKGRGTUC3XQNC33YTU6SLZ3PBY3AVCNFSM6AAAAABPT2YBB2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMJRGI4DONRWHE . > You are receiving this because you authored the thread.Message ID: > @.***> >

— Reply to this email directly, view it on GitHub https://github.com/guretskiysemyon/k-coloringReduction/issues/2#issuecomment-2414550904, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADAKGRE2Y7AXTFIF67QY7E3Z3VCWRAVCNFSM6AAAAABPT2YBB2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMJUGU2TAOJQGQ . You are receiving this because you authored the thread.Message ID: @.***>