1

SAT ソルバーに必要な形式に操作する必要がある DIMACS cnf 形式のファイルがあります。

具体的には、次のものを取得する必要があります。

['c horn? no', 'c forced? no', 'c mixed sat? no', 'c clause length = 3', 'c', 'p cnf 20  91', '4 -18 19 0', '3 18 -5 0', '-5 -8 -15 0', '-20 7 -16 0']

に

[[4,-18,19,0], [3,18,-5,0],[-5,-8,-15,0],[-20,7,-16,0]]

助けてくれてありがとう！

4

1 に答える 1

3

簡単なハックとして、簡単に使用できます

in_data = ['c horn? no', 'c forced? no', 'c mixed sat? no', 'c clause length = 3', 'c', 'p cnf 20  91', '4 -18 19 0', '3 18 -5 0', '-5 -8 -15 0', '-20 7 -16 0']
out_data = [[int(n) for n in line.split()] for line in in_data if line[0] not in ('c', 'p')]
print(out_data)

どちらが出力されますか

[[4, -18, 19, 0], [3, 18, -5, 0], [-5, -8, -15, 0], [-20, 7, -16, 0]]

ただし、次のようなものを使用したい場合があります

out_data = [[int(n) for n in line.split() if n != '0'] for line in in_data if line[0] not in ('c', 'p')]

代わりに、句から末尾のゼロを削除します。

[[4, -18, 19], [3, 18, -5], [-5, -8, -15], [-20, 7, -16]]

しかし、実際の dimacs パーサーは、1 行に 1 つの句を想定するのではなく、実際には終端のゼロを使用する必要があります。したがって、ここに適切な dimacs パーサーがあります。

in_data = ['c horn? no', 'c forced? no', 'c mixed sat? no', 'c clause length = 3', 'c', 'p cnf 20  91', '4 -18 19 0', '3 18 -5 0', '-5 -8 -15 0', '-20 7 -16 0']

cnf = list()
cnf.append(list())
maxvar = 0

for line in in_data:
    tokens = line.split()
    if len(tokens) != 0 and tokens[0] not in ("p", "c"):
        for tok in tokens:
            lit = int(tok)
            maxvar = max(maxvar, abs(lit))
            if lit == 0:
                cnf.append(list())
            else:
                cnf[-1].append(lit)

assert len(cnf[-1]) == 0
cnf.pop()

print(cnf)
print(maxvar)
于 2015-05-12T03:00:16.847 に答える