TypeError

[daajoe]

[INFO] Number of Var : 2 [INFO] Number of Clause: 4 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [INFO] Satisfying probabilty = None Traceback (most recent call last): File "/home/h7/jfichte/mc_reprobench/experiment/mc2021/0-mc2020/track1/2021-ntu-jiang/bin/ssatABC.p\ y", line 55, in count = (float(prob) * pow(2, (var_num))) TypeError: float() argument must be a string or a number, not 'NoneType'

Instance was: c t mc p cnf 2 4 1 -2 0 -1 2 0 -1 -2 0 1 2 0

[daajoe]

Same problem with a satisfiable instance.

[nianzelee]

@haorenW1025 This seems to be a problem with the converting script. Could you please take a look?

[nianzelee]

Ah okay, I found the problem. It is because the SSAT solver does a sanity check of the prefixes, and it only accepts random-exist and exist-random quantified SSAT formulas. It is probably not a problem with the conversion script. This would mean we may only be able to participate in the PMC track, which translates to random-exist quantified SSAT formulas.

[daajoe]

In principle, you should be able to quantify over all the existing variables by just manually giving them to the solver, right?

[nianzelee]

Yes, but in practice, our SSAT solver does not work this way now. Modifying the solver to accept a pure randomly quantified formula would take some time, and it might not be worth the effort because this collapses to model counting with BDDs. I will make sure our solver works with PMC. With MC and WMC tracks, please allow us to discuss if it is meaningful to participate.

[haorenW1025]

I think the issue is in the converting script. I've changed the temporary file path but forget to modify some function's arguments. @daajoe Can you try again with the newest commit?

@nianzelee I've noticed the issue that you mentioned here, but I've made a hack to create a dummy exist variable to avoid the issues. Do you think this hack would cause any problems? The solving result seems to be correct with this hack.

[haorenW1025]

@nianzelee FYI the hack I mentioned above: https://github.com/NTU-ALComLab/MCC2021/blob/e7bd5b7e0777aae9fcaa9eca5b0a425e29d2a0c0/bin/parser.py#L93-L95

[nianzelee]

@nianzelee FYI the hack I mentioned above: https://github.com/NTU-ALComLab/MCC2021/blob/e7bd5b7e0777aae9fcaa9eca5b0a425e29d2a0c0/bin/parser.py#L93-L95

Okay, this could be a workaround.

[nianzelee]

I tried in ./bin the following PMC file with python3 ssatABC.py ../pmc.dimacs ../pmc.sdimacs ../output.log,

p cnf 2 4 1 
c t pmc
c p show 1 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

I still got a TypeError. The converted sdimacs file looks strange:

p cnf 3 4
e 3 0
e 2 0
r 0.5 1 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

Why is it an exist-random SSAT? Did I get anything wrong?

[haorenW1025]

I tried in ./bin the following PMC file with python3 ssatABC.py ../pmc.dimacs ../pmc.sdimacs ../output.log,

p cnf 2 4 1 
c t pmc
c p show 1 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

I still got a TypeError.

The TypeError here seems to be related to a not correctly handled regex, should be fixed in the commit 79b4379

The converted sdimacs file looks strange:

p cnf 3 4
e 3 0
e 2 0
r 0.5 1 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

Why is it an exist-random SSAT? Did I get anything wrong?

The exist variable come from the not-projected variables in the original dimacs, but the hack I mentioned above is still applied to the PMC cases which should be fixed. The random variable comes from the projected variable and the probability is 0.5. Is there anything wrong with my interpretation?

[nianzelee]

I tried in ./bin the following PMC file with python3 ssatABC.py ../pmc.dimacs ../pmc.sdimacs ../output.log,

p cnf 2 4 1 
c t pmc
c p show 1 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

I still got a TypeError.

The TypeError here seems to be related to a not correctly handled regex, should be fixed in the commit 79b4379

The converted sdimacs file looks strange:

p cnf 3 4
e 3 0
e 2 0
r 0.5 1 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

Why is it an exist-random SSAT? Did I get anything wrong?

The exist variable come from the not-projected variables in the original dimacs, but the hack I mentioned above is still applied to the PMC cases which should be fixed. The random variable comes from the projected variable and the probability is 0.5. Is there anything wrong with my interpretation?

I would expect the converted sdimacs file like the following

p cnf 2 4
r 0.5 1 0
e 2 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

Note that the random variables (projected) come before the existential variables (non-projected).

[haorenW1025]

I would expect the converted sdimacs file like the following

p cnf 2 4
r 0.5 1 0
e 2 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

Note that the random variables (projected) come before the existential variables (non-projected).

Should be fixed by the latest commit.

[nianzelee]

I would expect the converted sdimacs file like the following

p cnf 2 4
r 0.5 1 0
e 2 0
1 -2 0
-1 2 0
-1 -2 0
1 2 0

Note that the random variables (projected) come before the existential variables (non-projected).

Should be fixed by the latest commit.

I still got a TypeError

[INFO] Number of Var   : 2
[INFO] Number of Clause: 4
[INFO] Finished converting MCC 2021 format into sdimacs
[INFO] Running SSAT solver...
[INFO] Satisfying probabilty = 0.000000e+00
Traceback (most recent call last):
  File "ssatABC.py", line 49, in <module>
    write_result(sys.argv[3], count)
TypeError: write_result() missing 1 required positional argument: 'counter_type'

Function write_result() in bin/parser.py has a third argument counter_type, but it is never given in bin/ssatABC.py.

[haorenW1025]

Ah sorry my bad, I forgot to include ssatABC.py in the latest commit, should be fixed now.

[nianzelee]

I tested against the following WMC example from the competition description file:

c c This file describes a weighted CNF in MC 2021 format
c c with 6 variables and 4 clauses
p cnf 6 4
c t wmc
c c Weights are given as follows, spaces may be added
c c to improve readability.
c p weight 1 0.4 0
c p weight 2 0.5 0
c p weight 3 0.4 0
c p weight 4 0.3 0
c p weight 5 0.5 0
c p weight 6 0.7 0
-1 -2 0
2 3 -4 0
c this is a comment and will be ignored
4 5 0
4 6 0
c same

I got the following error:

[INFO] Number of Var   : 6
[INFO] Number of Clause: 4
[INFO] Finished converting MCC 2021 format into sdimacs
[INFO] Running SSAT solver...
[INFO] Satisfying probabilty = 3.460000e-01
[INFO] SATISFIABLE with model count = 3.460000e-01
Traceback (most recent call last):
  File "ssatABC.py", line 52, in <module>
    write_result(sys.argv[3], count, counter_type)
  File "/home/nianzelee/Research/Software/MCC2021/bin/parser.py", line 131, in write_result
    f.write("c s exact arb float {}\n".format(int(res)))
ValueError: invalid literal for int() with base 10: '3.460000e-01'

@haorenW1025 Could you please take a look?

[nianzelee]

The script computes correct answers for the MC and PMC examples.

[haorenW1025]

I tested against the following WMC example from the competition description file:

c c This file describes a weighted CNF in MC 2021 format
c c with 6 variables and 4 clauses
p cnf 6 4
c t wmc
c c Weights are given as follows, spaces may be added
c c to improve readability.
c p weight 1 0.4 0
c p weight 2 0.5 0
c p weight 3 0.4 0
c p weight 4 0.3 0
c p weight 5 0.5 0
c p weight 6 0.7 0
-1 -2 0
2 3 -4 0
c this is a comment and will be ignored
4 5 0
4 6 0
c same

I got the following error:

[INFO] Number of Var   : 6
[INFO] Number of Clause: 4
[INFO] Finished converting MCC 2021 format into sdimacs
[INFO] Running SSAT solver...
[INFO] Satisfying probabilty = 3.460000e-01
[INFO] SATISFIABLE with model count = 3.460000e-01
Traceback (most recent call last):
  File "ssatABC.py", line 52, in <module>
    write_result(sys.argv[3], count, counter_type)
  File "/home/nianzelee/Research/Software/MCC2021/bin/parser.py", line 131, in write_result
    f.write("c s exact arb float {}\n".format(int(res)))
ValueError: invalid literal for int() with base 10: '3.460000e-01'

@haorenW1025 Could you please take a look?

Should be fixed now, WMC cases should output float type but the variable is assign as integer.

[nianzelee]

Yes, I can confirm. I will add a target to the Makefile to run the three examples from the competition description file. It will be easier for Johannes to confirm the correctness of the solver.

[nianzelee]

@daajoe Could you please take a look at commit 9af2309? You should be able to run the solver in the directory "./bin" as follows:

./starexec_run_default ../examples/mc.dimacs ../mc.sdimacs ../mc.log
./starexec_run_default ../examples/wmc.dimacs ../wmc.sdimacs ../wmc.log
./starexec_run_default ../examples/pmc.dimacs ../pmc.sdimacs ../pmc.log

Please let us know if there are any further execution problems.

@haorenW1025 Thank you for the great work!

[nianzelee]

I updated the readme so that it is easier to see how to run the solver.

[daajoe]

p cnf 2 3 c t pmc c p show 1 2 0 1 2 0 1 -2 0 -1 -2 0

gives Running the default configuration ... Input file: ../examples/pmc.dimacs Converted SSAT file: ../pmc.sdimacs Output file: ../pmc.log [INFO] Number of Var : 2 [INFO] Number of Clause: 3 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [ERROR] Currently only support "{RE,ER}-2SSAT"! [INFO] Satisfying probabilty = None Traceback (most recent call last): File "ssatABC.py", line 48, in count = (float(prob) * pow(2, (len(projected)))) TypeError: float() argument must be a string or a number, not 'NoneType'

[daajoe]

wmc and mc look good. Relative paths don't work on the cluster in Dresden. But we can figure that out later. Could you try it out first yourself on StarExec, might work there. You should be able to create a solver and job in the respective communties.

Note that the script on starexec should just get $1 as parameter.

So inside the script you could create the tempfiles and make sure that they are deleted by:

function finish {
  # Your cleanup code here
    [ ! -z "$TMP_OUT" ] && rm $TMP_OUT
    [ ! -z "$TMP_OUT2" ] && rm $TMP_OUT2
    echo "c o Removing tmp files"
}
trap finish EXIT
trap interrupted TERM
trap interrupted INT

TMP_OUT=$(mktemp)
TMP_OUT2=$(mktemp)

#run your python script
python3 ssat.py $1 $TMP_OUT $TMP_OUT2

[nianzelee]

p cnf 2 3 c t pmc c p show 1 2 0 1 2 0 1 -2 0 -1 -2 0

gives Running the default configuration ... Input file: ../examples/pmc.dimacs Converted SSAT file: ../pmc.sdimacs Output file: ../pmc.log [INFO] Number of Var : 2 [INFO] Number of Clause: 3 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [ERROR] Currently only support "{RE,ER}-2SSAT"! [INFO] Satisfying probabilty = None Traceback (most recent call last): File "ssatABC.py", line 48, in count = (float(prob) * pow(2, (len(projected)))) TypeError: float() argument must be a string or a number, not 'NoneType'

@haorenW1025 If all of the variables of a PMC instance are projected variables, the script generates an SSAT formula with only random quantification. Could you fix this by the workaround discussed above?

[nianzelee]

wmc and mc look good. Relative paths don't work on the cluster in Dresden. But we can figure that out later. Could you try it out first yourself on StarExec, might work there. You should be able to create a solver and job in the respective communties.

Note that the script on starexec should just get $1 as parameter.

So inside the script you could create the tempfiles and make sure that they are deleted by:

function finish {
  # Your cleanup code here
    [ ! -z "$TMP_OUT" ] && rm $TMP_OUT
    [ ! -z "$TMP_OUT2" ] && rm $TMP_OUT2
    echo "c o Removing tmp files"
}
trap finish EXIT
trap interrupted TERM
trap interrupted INT

TMP_OUT=$(mktemp)
TMP_OUT2=$(mktemp)

#run your python script
python3 ssat.py $1 $TMP_OUT $TMP_OUT2

Thanks for the information. We will try it out.

[haorenW1025]

p cnf 2 3 c t pmc c p show 1 2 0 1 2 0 1 -2 0 -1 -2 0

gives Running the default configuration ... Input file: ../examples/pmc.dimacs Converted SSAT file: ../pmc.sdimacs Output file: ../pmc.log [INFO] Number of Var : 2 [INFO] Number of Clause: 3 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [ERROR] Currently only support "{RE,ER}-2SSAT"! [INFO] Satisfying probabilty = None Traceback (most recent call last): File "ssatABC.py", line 48, in count = (float(prob) * pow(2, (len(projected)))) TypeError: float() argument must be a string or a number, not 'NoneType'

@daajoe Thanks for the input. This issue should be fixed in the lastest commit. The example pmc benchmark is added into the example directory in the repo.

[daajoe]

(base) jfichte@comp:/projects/tmp_mcc2021/solvers/MCC2021/bin$ ./starexec_run_default ../examples/pmc.dimacs ../pmc.sdimacs ../pmc.log Running the default configuration ... Input file: ../examples/pmc.dimacs Converted SSAT file: ../pmc.sdimacs Output file: ../pmc.log [INFO] Number of Var : 6 [INFO] Number of Clause: 4 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [INFO] Satisfying probabilty = 7.500000e-01 [INFO] SATISFIABLE with model count = 3.0

Looks good now. But using another path gives: (base) jfichte@perdix:/projects/tmp_mcc2021/solvers/MCC2021/bin$ ./starexec_run_default ../examples/pmc.dimacs /tmp/test1 /tmp/test2 Running the default configuration ... Input file: ../examples/pmc.dimacs Converted SSAT file: /tmp/test1 Output file: /tmp/test2 [INFO] Number of Var : 6 [INFO] Number of Clause: 4 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [INFO] Satisfying probabilty = None Traceback (most recent call last): File "ssatABC.py", line 48, in count = (float(prob) * pow(2, (len(projected)))) TypeError: float() argument must be a string or a number, not 'NoneType'

[daajoe]

The configuration on StarExec will likely not work (https://www.starexec.org/starexec/secure/details/solver.jsp?id=32594). ssat.zip Would be good if you can follow the template as attached (however there I get the TypeError).

[nianzelee]

Looks good now. But using another path gives: (base) jfichte@perdix:/projects/tmp_mcc2021/solvers/MCC2021/bin$ ./starexec_run_default ../examples/pmc.dimacs /tmp/test1 /tmp/test2 Running the default configuration ... Input file: ../examples/pmc.dimacs Converted SSAT file: /tmp/test1 Output file: /tmp/test2 [INFO] Number of Var : 6 [INFO] Number of Clause: 4 [INFO] Finished converting MCC 2021 format into sdimacs [INFO] Running SSAT solver... [INFO] Satisfying probabilty = None Traceback (most recent call last): File "ssatABC.py", line 48, in count = (float(prob) * pow(2, (len(projected)))) TypeError: float() argument must be a string or a number, not 'NoneType'

This is because the solver requires the file extension of a converted file to be .sdimacs. Running starexec_run_default ../examples/pmc.dimacs /tmp/test1.sdimacs /tmp/test2 should work. @haorenW1025 Please remember to rename the tmp file in the starexec_run_default script.

[nianzelee]

The configuration on StarExec will likely not work (https://www.starexec.org/starexec/secure/details/solver.jsp?id=32594). ssat.zip Would be good if you can follow the template as attached (however there I get the TypeError).

We are still preparing a new upload. Hao-Ren will take care of it. @daajoe Could you please add him into the model-counting community? His email address is r09943108@ntu.edu.tw.

[daajoe]

Approved you on StarExec, but will have to ask Markus to add you to the subspaces and set permissions.

[haorenW1025]

@daajoe Small question here, in the example you gave above, you mentioned that starexec would only accept a single argument, how can we assign the output solution file here? For example, Running starexec_run_default ../examples/pmc.dimacs /tmp/test1.sdimacs /tmp/test2 would convert ../examples/pmc.dimacs into /tmp/test1.sdimacs and output the result into /tmp/test2. But if follow your suggestion script, tmp/test2 would be deleted, then how should the contest know whether our solution is correct or not?

[daajoe]

I see. Couldn't you just cat the output-file then? The result is expected to go to stdout anyways.

[nianzelee]

@haorenW1025 Any update? The submission deadline is today. Let me know if you need any help.

[daajoe]

Any updates?

[nianzelee]

@daajoe The solvers have been uploaded to StarExec.