CSReader doesn't throws a ContradictionException when adding conflicting clauses.
When parsing a CSP instance using XMLCSPReader, it doesn't throw a ContradictionException for conflicting clauses. It only prints a message to the console.
Ex:
...
XMLCSPReader reader = new XMLCSPReader(solver, true);
try { reader.parseInstance(file); // Console output: c INSTANCE TRIVIALLY UNSAT if(problem.isSatisfiable()){ // Returns true // } } catch (ContradictionException e) { System.out.println("Contradiction"); // Should be thrown by parseInstance }
The ContradictionException is catched by method endConstraint() in org.sat4j.CSPReader.java and it prints the message. After that happens there is no way of knowing it was TRIVIALLY UNSAY.