Package org.sat4j.specs

Those classes are intented for users dealing with SAT solvers as blackboxes.

See:
Description

Interface Summary

IConstr	The most general abstraction for handling a constraint.
IProblem	Access to the information related to a given problem instance.
ISolver	That interface contains all the services available on a SAT solver.
IVec<T>	An abstraction on the type of vector used in the library.
IVecInt	An abstraction for the vector of int used on the library.

Exception Summary

ContradictionException	That exception is launched whenever a trivial contradiction is found (e.g. null clause).
TimeoutException	Exception launched when the solver cannot solve a problem within its allowed time.

Package org.sat4j.specs Description

Those classes are intented for users dealing with SAT solvers as blackboxes.

        ISolver solver = SolverFactory.newMiniLearning();
        solver.setTimeout(3600); // 1 hour timeout
        Reader reader = new DimacsReader(solver);
        // CNF filename is given on the command line 
        try {
                IProblem problem = reader.parseInstance(args[0]);
                if (problem.isSatisfiable()) {
                        System.out.println("Satisfiable !");
                        System.out.println(reader.decode(problem.model()));
                } else {
                        System.out.println("Unsatisfiable !");
                }
        } catch (FileNotFoundException e) {
                // TODO Auto-generated catch block
        } catch (ParseFormatException e) {
                // TODO Auto-generated catch block
        } catch (IOException e) {
                // TODO Auto-generated catch block
        } catch (ContradictionException e) {
                System.out.println("Unsatisfiable (trivial)!");
        } catch (TimeoutException e) {
                System.out.println("Timeout, sorry!");          
        }