mcc2021's Introduction

MCC2021

Files to participate in the Model Counting Competition 2021

Usage

Execute the solver in the directory ./bin as follows:

./starexec_run_default <model counting dimacs file>

For example:

./starexec_run_default ../examples/pmc.dimacs

The script bin/ssatABC.py will convert a model counting instance from MCC2021 to an SSAT formula in sdimacs format and use a precompiled SSAT solver to solve it. A converted SSAT file is written to /tmp/ and will be cleaned after the execution.

Type make to generate an archive for uploading to StarExec.

mcc2021's People

Contributors

Stargazers

Watchers

mcc2021's Issues

Update the temporary path `write_sdimacs` to a parameter or do it in memory

As required by the competition organizers.

Use full names for commands and remove `abc.rc`

Let's remove abc.rc from the repository.
It is only needed for command aliases and we can just use full names for commands in the scripts.

@haorenW1025 : would you take care of this issue?

Compile `abc` without dynamic libraries

The competition organizers ran into the following problem caused by libreadline:

./abc: error while loading shared libraries: libreadline.so.8: cannot open shared object file: No such file or directory

It can be solved by compiling abc without libreadline, or without any dynamic libraries.

@haorenW1025 has already committed the former solution.
For the latter, we may need to change the Makefile of abc, to use options suggested by Johannes.

(gcc<4.4 g++ -static otherwise: gcc -static -static-libstdc++ -static-libgcc)

The files on StarExec have not been updated yet.

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 = 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

Recommend Projects