@Test public void testReadClauses() throws Exception { ProblemInstanceInfo pii = new ProblemInstanceInfo("uf20", ProblemInstanceOrigin.RESOURCE, "/org/seage/problem/sat/instances/uf20-01.cnf"); SatProblemProvider spp = new SatProblemProvider(); Formula formula = spp.initProblemInstance(pii); assertNotNull(formula); assertEquals(20, formula.getLiterals().size()); assertEquals(91, formula.getClauses().size()); assertEquals(3, formula.getClauses().get(0).getLiterals()[0].getIndex()); assertEquals(false, formula.getClauses().get(0).getLiterals()[0].isNeg()); assertEquals(17, formula.getClauses().get(0).getLiterals()[1].getIndex()); assertEquals(true, formula.getClauses().get(0).getLiterals()[1].isNeg()); assertEquals(18, formula.getClauses().get(0).getLiterals()[2].getIndex()); assertEquals(false, formula.getClauses().get(0).getLiterals()[2].isNeg()); assertEquals(13, formula.getClauses().get(45).getLiterals()[0].getIndex()); assertEquals(false, formula.getClauses().get(45).getLiterals()[0].isNeg()); assertEquals(6, formula.getClauses().get(45).getLiterals()[1].getIndex()); assertEquals(false, formula.getClauses().get(45).getLiterals()[1].isNeg()); assertEquals(9, formula.getClauses().get(45).getLiterals()[2].getIndex()); assertEquals(false, formula.getClauses().get(45).getLiterals()[2].isNeg()); assertEquals(3, formula.getClauses().get(90).getLiterals()[0].getIndex()); assertEquals(false, formula.getClauses().get(90).getLiterals()[0].isNeg()); assertEquals(15, formula.getClauses().get(90).getLiterals()[1].getIndex()); assertEquals(true, formula.getClauses().get(90).getLiterals()[1].isNeg()); assertEquals(4, formula.getClauses().get(90).getLiterals()[2].getIndex()); assertEquals(true, formula.getClauses().get(90).getLiterals()[2].isNeg()); }
public static List<Clause> readClauses(InputStream stream) throws IOException { LineNumberReader lnr = new LineNumberReader(new BufferedReader(new InputStreamReader(stream))); lnr.setLineNumber(1); StreamTokenizer stok = new StreamTokenizer(lnr); int[] dataLine = null; ArrayList<Clause> clauses = new ArrayList<Clause>(); while ((dataLine = readLine(stok)) != null) { if (dataLine.length < 3) { continue; } Literal[] literals = new Literal[3]; for (int i = 0; i < 3; i++) { boolean neg = dataLine[i] < 0 ? true : false; int ix = Math.abs(dataLine[i]) - 1; literals[i] = new Literal(ix, neg); } Clause newClause = new Clause(literals); clauses.add(newClause); } return clauses; }
FormulaReader { public static List<Clause> readClauses(InputStream stream) throws IOException { LineNumberReader lnr = new LineNumberReader(new BufferedReader(new InputStreamReader(stream))); lnr.setLineNumber(1); StreamTokenizer stok = new StreamTokenizer(lnr); int[] dataLine = null; ArrayList<Clause> clauses = new ArrayList<Clause>(); while ((dataLine = readLine(stok)) != null) { if (dataLine.length < 3) { continue; } Literal[] literals = new Literal[3]; for (int i = 0; i < 3; i++) { boolean neg = dataLine[i] < 0 ? true : false; int ix = Math.abs(dataLine[i]) - 1; literals[i] = new Literal(ix, neg); } Clause newClause = new Clause(literals); clauses.add(newClause); } return clauses; } }
FormulaReader { public static List<Clause> readClauses(InputStream stream) throws IOException { LineNumberReader lnr = new LineNumberReader(new BufferedReader(new InputStreamReader(stream))); lnr.setLineNumber(1); StreamTokenizer stok = new StreamTokenizer(lnr); int[] dataLine = null; ArrayList<Clause> clauses = new ArrayList<Clause>(); while ((dataLine = readLine(stok)) != null) { if (dataLine.length < 3) { continue; } Literal[] literals = new Literal[3]; for (int i = 0; i < 3; i++) { boolean neg = dataLine[i] < 0 ? true : false; int ix = Math.abs(dataLine[i]) - 1; literals[i] = new Literal(ix, neg); } Clause newClause = new Clause(literals); clauses.add(newClause); } return clauses; }  }
FormulaReader { public static List<Clause> readClauses(InputStream stream) throws IOException { LineNumberReader lnr = new LineNumberReader(new BufferedReader(new InputStreamReader(stream))); lnr.setLineNumber(1); StreamTokenizer stok = new StreamTokenizer(lnr); int[] dataLine = null; ArrayList<Clause> clauses = new ArrayList<Clause>(); while ((dataLine = readLine(stok)) != null) { if (dataLine.length < 3) { continue; } Literal[] literals = new Literal[3]; for (int i = 0; i < 3; i++) { boolean neg = dataLine[i] < 0 ? true : false; int ix = Math.abs(dataLine[i]) - 1; literals[i] = new Literal(ix, neg); } Clause newClause = new Clause(literals); clauses.add(newClause); } return clauses; }  static List<Clause> readClauses(InputStream stream); }
FormulaReader { public static List<Clause> readClauses(InputStream stream) throws IOException { LineNumberReader lnr = new LineNumberReader(new BufferedReader(new InputStreamReader(stream))); lnr.setLineNumber(1); StreamTokenizer stok = new StreamTokenizer(lnr); int[] dataLine = null; ArrayList<Clause> clauses = new ArrayList<Clause>(); while ((dataLine = readLine(stok)) != null) { if (dataLine.length < 3) { continue; } Literal[] literals = new Literal[3]; for (int i = 0; i < 3; i++) { boolean neg = dataLine[i] < 0 ? true : false; int ix = Math.abs(dataLine[i]) - 1; literals[i] = new Literal(ix, neg); } Clause newClause = new Clause(literals); clauses.add(newClause); } return clauses; }  static List<Clause> readClauses(InputStream stream);  }