Java에서 .cnf 파일을 읽는 방법

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#에서) 다음과 같다 :

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(); 
    } 

:

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; 
     } 
    } 
} 

는 CNF 라인에서 Clause 객체를 구성하는 데

이 의사 코드는 CNF이 Clause 개체의 목록으로 저장되어 있다고 가정합니다. 각 Clause은 Literal 개체의 목록입니다. Literal에는 양수 변수 ID과 반전되거나 역전 된 극성이 있습니다.

성능 측면에서 개체 목록이 아닌 정수 배열 (또는 비트 세트조차도)로 저장하는 것이 좋습니다.

Answer 2

라이브러리 SAT4J (http://www.sat4j.org/)를 사용하려는 경우 Java에서 .cnf를 아무 문제없이 읽을 수 있습니다.

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에게 공식을 해결하기 위해 설계되었습니다. 하지만 원하는대로 읽을 수는 있습니다 :).