import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
private int[] runSatSolver(Path path){
    ISolver solver = SolverFactory.newDefault();
    solver.setTimeout(TIMEOUT_MINUTES);
    Reader reader = new DimacsReader(solver);

    IProblem problem = null;
    try {
        problem = reader.parseInstance(path.toString());
        if (problem.isSatisfiable()) {
            return problem.model();
        } else {
            logger.error("Problem described in " + path.getFileName() + " is unsatisfiable");
        }
    } catch (ContradictionException | TimeoutException | ParseFormatException | IOException e) {
        logger.error("Error during SAT-solver processing", e);
    }
    return null;
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
@Before
public void setUp() throws FileNotFoundException, ParseFormatException,
		IOException, ContradictionException {
	xplain = new Xplain<ISolver>(SolverFactory.newDefault());
	xplain.setTimeout(3600); // 1 hour timeout
	Reader reader = new DimacsReader(xplain);
	String dimacs = "src/test/testfiles/eb42.dimacs";
	reader.parseInstance(dimacs);
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
@Test
public void testReaderFromDimacsReader() throws ParseFormatException,
		ContradictionException, IOException, TimeoutException {
	String cnfString = "p cnf 3 4\n1 2 3 0\n-1 -2 0\n-1 -3 0\n-2 -3 0";
	DimacsReader reader = new DimacsReader(SolverFactory.newDefault());
	IProblem problem = reader.parseInstance(new ByteArrayInputStream(
			cnfString.getBytes()));
	assertNotNull(problem);
	assertTrue(problem.isSatisfiable());
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
@Before
public void setUp() throws FileNotFoundException, ParseFormatException,
        IOException, ContradictionException {
    this.xplain = new Xplain<ISolver>(SolverFactory.newDefault());
    this.xplain.setTimeout(3600); // 1 hour timeout
    Reader reader = new DimacsReader(this.xplain);
    String dimacs = "src/test/testfiles/eb42.dimacs";
    reader.parseInstance(dimacs);
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
@Test
public void testReaderFromDimacsReader() throws ParseFormatException,
        ContradictionException, IOException, TimeoutException {
    String cnfString = "p cnf 3 4\n1 2 3 0\n-1 -2 0\n-1 -3 0\n-2 -3 0";
    DimacsReader reader = new DimacsReader(SolverFactory.newDefault());
    IProblem problem = reader.parseInstance(new ByteArrayInputStream(
            cnfString.getBytes()));
    assertNotNull(problem);
    assertTrue(problem.isSatisfiable());
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
public SAT4JSolver(String filename) throws FileNotFoundException, ParseFormatException, IOException, ContradictionException {
	solver = SolverFactory.newDefault();
	solver.setDBSimplificationAllowed(true);
       Reader reader = new DimacsReader(solver);
	reader.parseInstance(filename);
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
@Override
protected Reader createReader(ISolver theSolver, String problemname) {
    if (problemname.endsWith(".cnf"))
        return new DimacsReader(theSolver);
    return new OPBReader2012(handle);
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
public PerformanceResult answer(Reasoner r) {
	int iteration = 0;
	if (r == null) {
		throw new FAMAParameterException("Reasoner :Not specified");
	}

	features = new String[((Sat4jReasoner) r).getVariables().size()];
	cnfvalues = new String[((Sat4jReasoner) r).getVariables().size()];

	int i = 0;
	for (Entry<String, String> entry : ((Sat4jReasoner) r).getVariables().entrySet()) {
		features[i] = entry.getKey();
		cnfvalues[i] = entry.getValue();
		i++;
	}

	// prepare the reasoning mechanism
	String cnfmodel = ((Sat4jReasoner) r).getPartialCNF(1);
	solver = SolverFactory.newDefault();
	ModelIterator mi = new ModelIterator(solver);
	solver.setTimeout(3600); // 1 hour timeout
	Reader reader = new DimacsReader(mi);

	try {
		reader.parseInstance(new ByteArrayInputStream((cnfmodel).getBytes(StandardCharsets.UTF_8)));

		// First iteration
		PrintWriter out = new PrintWriter(outputDirectory + "/" + iteration + ".out");
		for (i = 0; i < features.length; i++) {
			if (isValidConf(i + 1)) {
				out.println((i + 1) + "\t" + features[i]);
			}
		}
		out.flush();
		out.close();

		// whatever it remains
		File file = new File(outputDirectory + "/" + iteration + ".out");
		while (file.length() > 0) {
			iteration++;

			try (BufferedReader br = new BufferedReader(new FileReader(file))) {
				String line;
				while ((line = br.readLine()) != null) {
					// process the line.

					String key = line.substring(0, line.indexOf('\t'));
					String value = line.substring(line.indexOf('\t') + 1, line.length());
					map(key, value, iteration);

				}
			}

			file = new File(outputDirectory + "/" + iteration + ".out");
		}

	} catch (ParseFormatException | ContradictionException | IOException e) {
		e.printStackTrace();
	}
	return null;
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
private boolean isConsistent(Collection<String> aC, List<String> notS) {
	
	
	//First we create the content of the cnf
	String cnf_content = "c CNF file\n";

	// We show as comments the variables's number
	Iterator<String> it = chReasoner.variables.keySet().iterator();
	while (it.hasNext()) {
		String varName = it.next();
		cnf_content += "c var " + chReasoner.variables.get(varName) + " = " + varName
				+ "\n";
	}

	// Start the problem
	cnf_content += "p cnf " + chReasoner.variables.size() + " " + (aC.size() + notS.size())
			+ "\n";
	// Clauses
	it = aC.iterator();
	while (it.hasNext()) {
		cnf_content += (String) it.next() + "\n";
	}

	it = notS.iterator();
	while (it.hasNext()) {
		cnf_content += (String) it.next() + "\n";
	}
	
	// End file
	cnf_content += "0";
	ByteArrayInputStream stream= new ByteArrayInputStream(cnf_content.getBytes(StandardCharsets.UTF_8));
	
	
	
	ISolver s = SolverFactory.newDefault();
	Reader reader = new DimacsReader(s);
	try {
		reader.parseInstance(stream);
		return s.isSatisfiable();
	} catch (TimeoutException | ParseFormatException | ContradictionException | IOException e) {
		e.printStackTrace();
		
	}
	return false;
	
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
private boolean isConsistent(Collection<String> aC) {
	
	
	//First we create the content of the cnf
	String cnf_content = "c CNF file\n";

	// We show as comments the variables's number
	Iterator<String> it = reasoner.variables.keySet().iterator();
	while (it.hasNext()) {
		String varName = it.next();
		cnf_content += "c var " + reasoner.variables.get(varName) + " = " + varName
				+ "\n";
	}

	// Start the problem
	cnf_content += "p cnf " + reasoner.variables.size() + " " + (-1+ relations.values().size())
			+ "\n";
	// Clauses
	it = relations.values().iterator();
	while (it.hasNext()) {
		cnf_content += (String) it.next() + "\n";
	}

	// End file
	cnf_content += "0";
	ByteArrayInputStream stream= new ByteArrayInputStream(cnf_content.getBytes(StandardCharsets.UTF_8));
	
	
	
	ISolver s = SolverFactory.newDefault();
	Reader reader = new DimacsReader(s);
	try {
		reader.parseInstance(stream);
		return s.isSatisfiable();
	} catch (TimeoutException | ParseFormatException | ContradictionException | IOException e) {
		e.printStackTrace();
		
	}
	return false;
	
}
 

import org.sat4j.reader.DimacsReader; //导入依赖的package包/类
public SAT4J() {
    ISolver solver = SolverFactory.newLight();
    solver.setTimeout(3600); // 1 hour timeout
    reader = new DimacsReader(solver);
}