Как читать файл .cnf в java

Question

У меня есть .cnf-файл, который содержит числа как Conjunctive Normal Form.

Мне нужно прочитать и сохранить их в структуре данных (матрице или списке), чтобы иметь возможность работать с ними в качестве индекса. (Мне нужно это, чтобы решить проблему с 3-SAT.)

Как я могу читать и хранить их на Java?

c This Formular is generated by mcnf 
c 
c horn? no 
c forced? no 
c mixed sat? no 
c clause length = 3 
c 
p cnf 20 91 
10 -3 16 0 
-8 20 -19 0 
2 -6 -20 0 
-7 9 3 0 
3 15 -14 0 
4 15 20 0 
11 -9 -6 0 
3 -17 19 0 
11 5 -12 0 
10 3 -15 0 
2 15 18 0 
-15 12 11 0 
18 -19 -8 0 
13 20 9 0 
11 -10 -14 0 
4 18 -9 0 
-7 -17 5 0 
-7 11 -15 0 
6 2 20 0 
16 -18 -17 0 
4 -13 -20 0 
11 17 -8 0 
13 -11 -9 0 
-11 13 19 0 
12 -19 14 0 
10 -1 -20 0 
19 -20 13 0 
13 2 11 0 
17 19 -18 0 
19 -20 -10 0 
-18 16 15 0 
-18 7 -20 0 
1 -14 -17 0 
1 -11 -18 0 
-18 8 13 0 
-8 4 16 0 
-10 1 13 0 
9 3 -20 0 
-13 4 8 0 
17 -11 18 0 
18 20 2 0 
-20 -1 4 0 
-19 2 -9 0 
-9 -16 -15 0 
-2 12 9 0 
5 19 6 0 
-8 -5 -13 0 
-18 20 -6 0 
5 -18 12 0 
2 5 19 0 
-5 -8 -11 0 
-20 -17 11 0 
-18 -14 -16 0 
-3 -18 -7 0 
-11 20 17 0 
-1 -15 -13 0 
9 -5 11 0 
-17 -7 -1 0 
-6 -1 -16 0 
-3 -15 -19 0 
17 14 11 0 
-17 12 13 0 
16 12 -2 0 
14 10 -16 0 
8 -4 5 0 
-5 16 17 0 
-18 -1 -15 0 
11 -15 -13 0 
16 -9 -7 0 
-8 -15 2 0 
-19 -10 1 0 
12 -15 -20 0 
13 -10 9 0 
17 7 18 0 
20 15 -2 0 
-6 -7 -1 0 
14 11 15 0 
18 13 -9 0 
-4 -12 -2 0 
-13 -5 -9 0 
5 13 16 0 
20 -14 -15 0 
19 -20 18 0 
19 -17 13 0 
3 19 14 0 
6 3 20 0 
-8 -20 -2 0 
12 -10 -19 0 
-2 -5 -8 0 
13 -4 -11 0 
-5 -10 19 0 
% 
0 

Answer 1

С точки зрения птиц ракурса, код псевдо CNF читатель выглядит следующим образом (в C#):

StreamReader cnf = openReader(fileName); 
int noOfVars = 0; 

while (!cnf.EndOfStream) 
{ 
    line = cnf.ReadLine().Trim(); 

    if (line.Length >= 1) 
    { 
     c = line[0]; 
     if ((noOfVars > 0) && 
      ((c == '-') || ((c >= '0') && (c <= '9')))) 
     { 
      Clause cl = new Clause(line); 

      ListOfClauses.Add(cl); 
     } 
     else if (c == 'c') 
     { 
      processCStatement(line); 
     } 
     else if (c == 'p') 
     { 
      processPStatement(line, ref noOfVars, ref noOfClauses); 
     } 
     else 
     { 
      error("Statement has neither 'c' nor 'p' in first column: " + line[0]); 
      break; 
     } 
    } 
} 

Для построения Clause объекта из CNF линии:

public Clause(string line) 
{ 
     int id = -1; 
     string[] arr = line.Split(whitespaceSeparator, StringSplitOptions.RemoveEmptyEntries); 

     if (arr.Length < 1) 
     { 
      raise("Empty clause!"); 
     } 

     foreach (string s in arr) 
     { 
      try 
      { 
       id = int.Parse(s); 
      } 
      catch (Exception) 
      { 
       raise("Invalid literal: " + s); 
      } 

      if (id != 0) 
      { 
       Literal lit = new Literal(id); 
       this.Add(lit); 
      } 
     } 

     if (id != 0) 
     { 
      raise("Line does not end with '0'"); 
     } 

     // sort literals and remove duplicates 
     this.unify(); 
    } 

Этот псевдокод предполагает, что CNF ist хранится в виде списка из Clause объектов. Каждый Clause представляет собой список объектов Literal. A Literal имеет положительную переменную ID и инвертированную или не инвертированную полярность.

Что касается производительности, возможно, лучше хранить литералы как целые массивы (или даже бит-множества), а не как список объектов.

Answer 2

Если вы хотите использовать библиотеку SAT4J (http://www.sat4j.org/), она будет читать .cnf в Java без каких-либо проблем.

public class Example { 

    public static void main(String[] args) { 
     ISolver solver = SolverFactory.newDefault(); 
     Reader reader = new DimacsReader(solver);  
     // CNF filename is given on the command line 
     try { 
      IProblem problem = reader.parseInstance(args[0]); 
     } catch (FileNotFoundException e) { 

     } catch (ParseFormatException e) { 

     } catch (IOException e) { 

     } 
    } 
} 

Эта библиотека предназначена для чтения и решения формулы CNF :). Но вы можете использовать его только для чтения, как вы хотели :).