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!");          
        }