search

sat-heritage / docker-images

SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers
MIT License
38 stars 3 forks source link

Execution issues with pprobsat:2014 #29

Open pauleve opened 2 years ago

pauleve commented 2 years ago 
+ docker run --name satex27913 --rm -e TIMEOUT=10 -v /home/runner/work/docker-images/docker-images/tests:/data satex/pprobsat:2014 aim-200-1_6-yes1-1.cnf
cnf...#### pprobsat:2014 ####
+ cd /solvers/pprobSAT
+ set +x
+ timeout 10 python .//pprobSAT.py /data/aim-200-1_6-yes1-1.cnf 1234567 12 /tmp
! satex/pprobsat:2014 timeout
ok (TIMEOUT)
+ docker run --name satex27913 --rm -e TIMEOUT=10 -v /home/runner/work/docker-images/docker-images/tests:/data satex/pprobsat:2014 aim-200-1_6-yes1-1.cnf.gz
gz...#### pprobsat:2014 ####
+ cd /solvers/pprobSAT
+ set +x
+ timeout 10 python .//pprobSAT.py /data/aim-200-1_6-yes1-1.cnf.gz 1234567 12 /tmp
c pprobSAT SC14
c Adrian Balint, Uwe Schöning
c runs n instances of probSAT in parallel
c running with PID 23
c found 5parameters
c starting 12 instances of probSAT with seed 1234567 on instance /data/aim-200-1_6-yes1-1.cnf.gz 
c writing temp files to  /tmp/
c starting instance 0 of probSAT started with seed 2068334374
c writing to files /tmp/probsat_2068334374.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '2068334374']
c started probSAT instance with PID24
c starting instance 1 of probSAT started with seed 506232513
c writing to files /tmp/probsat_506232513.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '506232513']
c started probSAT instance with PID25
c starting instance 2 of probSAT started with seed 1248725493
c writing to files /tmp/probsat_1248725493.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '1248725493']
c started probSAT instance with PID26
c starting instance 3 of probSAT started with seed 486877169
c writing to files /tmp/probsat_486877169.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '486877169']
c started probSAT instance with PID27
c starting instance 4 of probSAT started with seed 2075738457
c writing to files /tmp/probsat_2075738457.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '2075738457']
c started probSAT instance with PID28
c starting instance 5 of probSAT started with seed 1313206768
c writing to files /tmp/probsat_1313206768.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '1313206768']
c started probSAT instance with PID29
c starting instance 6 of probSAT started with seed 159143120
c writing to files /tmp/probsat_159143120.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '159143120']
c started probSAT instance with PID30
c starting instance 7 of probSAT started with seed 1147267742
c writing to files /tmp/probsat_1147267742.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '1147267742']
c started probSAT instance with PID31
c starting instance 8 of probSAT started with seed 1297657472
c writing to files /tmp/probsat_1297657472.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '1297657472']
c started probSAT instance with PID32
c starting instance 9 of probSAT started with seed 1685926622
c writing to files /tmp/probsat_1685926622.out .err
c calling probSAT with ['./probSAT', '-a', '/data/aim-200-1_6-yes1-1.cnf.gz', '1685926622']
c started probSAT instance with PID33
c starting instance 0 of probSAT started with seed 1774660115
c writing to files /tmp/probsat_1774660115.out .err
c calling probSAT with ['./probSAT', '-a', '--maxflips', '10000000', '/data/aim-200-1_6-yes1-1.cnf.gz', '1774660115']
c started probSAT instance with PID34
c starting instance 1 of probSAT started with seed 376133325
c writing to files /tmp/probsat_376133325.out .err
c calling probSAT with ['./probSAT', '-a', '--maxflips', '100000000', '/data/aim-200-1_6-yes1-1.cnf.gz', '376133325']
c started probSAT instance with PID35
c finished 35 with return value 2560
c signal: 0 exit code: 10
c winner seed: 376133325
c No parameter line found! Computing number of atoms and number of clauses from file!
c numVars: 0 numClauses: 0

c instance name       :  /data/aim-200-1_6-yes1-1.cnf.gz
c number of variables :  0
c number of literals  :  0
c number of clauses   :  0
c MaxNumOccurences    :  0
c MaxClauseSize       :  0
c MinClauseSize       :  10000
c Ratio               :    -nan

c probSAT SC14 parameteres: 
c using:              : only break          
c using:              : polynomial function 
c cb1                 : 2.060000
c cb2                 : 0.000000
c function:           : probsBreak[break] = pow((eps + break), -cb1)*pow((eps + break), -cb2);
c eps                 : 0.900000
c using:              : caching of break values
c XOR implementation  : yes
Traceback (most recent call last):
  File ".//pprobSAT.py", line 146, in <module>
    os.kill(-p, 15)
OSError: [Errno 3] No such process
c using:              : random clause selection

c general parameteres: 
c maxTries            : 9223372036854775807
c maxFlips            : 100000000
c seed                : 376133325
c -->Starting solver  : 

c EndStatistics:
c numFlips                      : 0        
c avg. flips/variable           : -nan    
c avg. flips/clause             : -nan    
c totalTries                    : 0        
c totalFlips                    : 0        
c flips/sec                     : -nan    
c Total CPU Time                : 0.000   sec
s SATISFIABLE
v 
ERROR Solver failed with return code 1