parse dimacs CNF-файл python

Question

У меня есть файл в формате DIMACS cnf, который мне нужно манипулировать в необходимом формате для SAT Solver.

В частности, мне нужно получить:

['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]] 

Спасибо за помощь!

Answer 1

как быстрый хак вы можете просто использовать

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 должен фактически использовать оканчивающийся нуль вместо того, чтобы принимать одно предложение в строке. так вот собственно 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)