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.
IOptimizationProblem Represents an optimization problem.
IProblem Access to the information related to a given problem instance.
ISolver This interface contains all services provided by a SAT solver.
IteratorInt Iterator interface to avoid boxing int into Integer.
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.
SearchListener Interface to the solver main steps.
 

Class Summary
Lbool That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.
 

Exception Summary
ContradictionException That exception is launched whenever a trivial contradiction is found (e.g.
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.defaultSolver();
        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!");          
        }



Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.