R-O-C-K-E-T/Factorio-SAT

.cnf file

DoINeedATag opened this issue · 3 comments

DoINeedATag commented

Hello,

I am rather out of my depth here, but I was messing around with different solvers to see if any were faster or slower than others. I found a couple GPU accelerated solvers https://github.com/nicolasprevot/GpuShareSat and https://github.com/muhos/ParaFROST, however they do no support input on STDIN. I thought it would be interesting to try these. Is it possible to output to a .cnf file to use these solvers?

DoINeedATag commented

Turns out GpuShareSat accepts STDIN, I just had to make sure the output was turned on -model for belt_balancer_net_free.py to work correctly.

However ParaFROST does not accept STDIN.
I was able to create what I think was a workaround for not being able to get a .cnf file.
I made a file with: cat > /home/input.cnf called save.sh and used it in --solver="cmd:./save.sh" I now have the .cnf format.

The issue now is belt_balancer_net_free.py does not seem to work with two file paths inside it from what I can tell. (I am assuming this because I was trying the same method for GpuShareSat providing the input file and once I dropped the input file on accident it worked without a hitch receiving data from STDIN and being able to output)

GpuShareSat with file input

clusterio@clusterio-master:~/Factorio-SAT-main$ python belt_balancer_net_free.py 10 10 4 4 --underground-length 6 --solver "cmd:/home/clusterio/GpuShareSat-master/rel-newtech/gpu/rel-newtech-gpu /home/clusterio/input.cnf -model -max-memory=60000 -max-thread-count=18" | python render.py
pygame 2.1.2 (SDL 2.0.16, Python 3.10.6)
Hello from the pygame community. https://www.pygame.org/contribute.html
Traceback (most recent call last):
  File "/home/clusterio/Factorio-SAT-main/belt_balancer_net_free.py", line 402, in <module>
    for solution in grid.itersolve(solver=args.solver, ignore_colour=True):
  File "/home/clusterio/Factorio-SAT-main/template.py", line 406, in itersolve
    solution = run_command_solver(solver[4:], self.clauses)
  File "/home/clusterio/Factorio-SAT-main/template.py", line 87, in run_command_solver
    formula.to_fp(io.TextIOWrapper(process.stdin))
  File "/home/clusterio/.local/lib/python3.10/site-packages/pysat/formula.py", line 736, in to_fp
    print(' '.join(str(l) for l in cl), '0', file=file_pointer)
BrokenPipeError: [Errno 32] Broken pipe
2.511676073074341
No solutions

GpuShareSat without file input

clusterio@clusterio-master:~/Factorio-SAT-main$ python belt_balancer_net_free.py 10 10 4 4 --underground-length 6 --solver "cmd:/home/clusterio/GpuShareSat-master/rel-newtech/gpu/rel-newtech-gpu  -model -max-memory=60000 -max-thread-count=18" | python render.py
pygame 2.1.2 (SDL 2.0.16, Python 3.10.6)
Hello from the pygame community. https://www.pygame.org/contribute.html
c
c This is glucose-gpu 1.0 --  based on MiniSAT (Many thanks to MiniSAT team)
c
c Reading from standard input... Use '--help' for help.
c Setting block count guideline to 20 (twice the number of multiprocessors)

c Parse cpu time:         0.02 s
c Eliminated clauses: 0.0195465 Mb
c Reduced to 4169 vars, 73513 cls (grow=0)
c No iterative elimination performed. (vars=4169, c/v ratio=17.6)
c |  Automatic Adjustement of the number of solvers. MaxMemory=60000, MaxCores= 18.                       |
c |  One Solver is taking 8.77Mb... Let's take 18 solvers for this run (max 40% of the maxMemory).       |
c |  all clones generated. Memory = 9135.62Mb
All solvers launched
c thread 0 found answer 0
c printing final stats
c A thread is exiting
c thread 14 found answer 0
c A thread is exiting
c thread 4 found answer 0
c A thread is exiting
c thread 6 found answer 0
c A thread is exiting
c thread 15 found answer 0
c A thread is exiting
c thread 3 found answer 0
c A thread is exiting
c thread 8 found answer 0
c A thread is exiting
c thread 7 found answer 0
c A thread is exiting
c thread 9 found answer 0
c A thread is exiting
c thread 12 found answer 0
c A thread is exiting
c thread 17 found answer 0
c A thread is exiting
c thread 16 found answer 0
c A thread is exiting
c thread 5 found answer 0
c A thread is exiting
c thread 11 found answer 0
c A thread is exiting
c thread 13 found answer 0
c A thread is exiting
c thread 10 found answer 0
c A thread is exiting
c thread 1 found answer 0
c A thread is exiting
c thread 2 found answer 0
c A thread is exiting
2.603959798812866

ParaFROST

clusterio@clusterio-master:~/Factorio-SAT-main$ python belt_balancer_net_free.py 10 10 4 4 --underground-length 6 --solver "cmd:/home/clusterio/ParaFROST-parafrost-3.2.2/build/gpu/parafrost /home/clusterio/input.cnf -model -modelprint -no-report" | python render.py
pygame 2.1.2 (SDL 2.0.16, Python 3.10.6)
Hello from the pygame community. https://www.pygame.org/contribute.html
Traceback (most recent call last):
  File "/home/clusterio/Factorio-SAT-main/belt_balancer_net_free.py", line 402, in <module>
    for solution in grid.itersolve(solver=args.solver, ignore_colour=True):
  File "/home/clusterio/Factorio-SAT-main/template.py", line 406, in itersolve
    solution = run_command_solver(solver[4:], self.clauses)
  File "/home/clusterio/Factorio-SAT-main/template.py", line 87, in run_command_solver
    formula.to_fp(io.TextIOWrapper(process.stdin))
  File "/home/clusterio/.local/lib/python3.10/site-packages/pysat/formula.py", line 736, in to_fp
    print(' '.join(str(l) for l in cl), '0', file=file_pointer)
BrokenPipeError: [Errno 32] Broken pipe
0.8243775367736816
No solutions
R-O-C-K-E-T commented

Factorio-SAT does have an option for sending problems to command solvers through a temporary file with the $FILE template argument (e.g. --solver 'cmd:my_solver $FILE').

For your examples:

python belt_balancer_net_free.py 10 10 4 4 --underground-length 6 --solver "cmd:/home/clusterio/GpuShareSat-master/rel-newtech/gpu/rel-newtech-gpu \$FILE -model -max-memory=60000 -max-thread-count=18" | python render.py
python belt_balancer_net_free.py 10 10 4 4 --underground-length 6 --solver "cmd:/home/clusterio/ParaFROST-parafrost-3.2.2/build/gpu/parafrost \$FILE -model -modelprint -no-report" | python render.py

When manually providing a input file, I think the issue was the solver not consuming standard input so Factorio-SAT failed to submit the problem.
You could fix that by using a script like:

cat > /dev/null
my-solver /path/to/problem.cnf

Or in a single step

cat > /path/to/problem.cnf
my-solver /path/to/problem.cnf

# Or with argument forwarding e.g. --solver "cmd:./run.sh arg"
#  my-solver /path/to/problem.cnf $@

If possible use standard input for entering problems, since it avoids slow disk writes.

ParaFROST also produces some funky models, so I've made the model parsing a bit more lenient to support that.

DoINeedATag commented

Your --solver 'cmd:my_solver \$FILE' solution works perfectly.

I have not tried your other suggestions, but I will be sure to. Can't hurt to have the practice.

I appreciate you taking the time and effort to explain this to me and to modify Factorio-SAT to work better with ParaFROST. I've had a lot of fun the last two days learning and struggling. The more you know though!

  • ❤️1