如何在java中读取.cnf文件答案

【问题标题】：How to read .cnf file in java如何在java中读取.cnf文件
【发布时间】：2016-06-09 03:22:41
【问题描述】：

我有一个 .cnf 文件，其中包含作为连接范式的数字。

我需要读取它们并将它们存储在数据结构（矩阵或列表）中，以便能够将它们用作索引。（我需要这个来解决一个 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

【问题讨论】：

如果您向搜索引擎询问“Java DIMACS”，您会得到this one。熟悉 CNF 的 DIMACS 格式。每个子句行都是以 0 结尾的文字列表。取反的文字被编码为负整数。 p 行指定变量和子句的数量。
@AxelKemper 我不知道 Dimacs 这个词，非常感谢！
@AxelKemper 感谢 Kahina 的来源。当我在 Google 上搜索 DIMACS 时，我找不到比它更好的解析器。但似乎我无法实现该代码，它太大了，而且我认为它的类/包是紧密耦合的！ :( 有更简单的方法吗？
Java + Dimacs，感觉有必要给你指点sat4j.org它会阅读并解决你的问题，有据可查，效率很高。

标签： java boolean satisfiability sat conjunctive-normal-form

【解决方案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;
       }
   }
}

从CNF 行构造Clause 对象：

 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 存储为 Clause 对象列表。每个Clause 都是Literal 对象的列表。 Literal 有一个正变量 ID 和一个反转或非反转极性。

就性能而言，将文字存储为整数数组（甚至位集）而不是对象列表可能会更好。

【讨论】：

OP 要求使用 Java，为什么要在 C# 中提出代码？
@ValentinMontmirail ：我的工具箱中有这段代码，并认为这是一个很好的练习和帮助 OP 入门。随时提供 Java 移植版本。

【解决方案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 公式:)。但是你可以用它来阅读你想要的内容:)。

【讨论】：