Package org.sat4j.specs

Those classes are intended for users dealing with SAT solvers as black boxes.

See: Description

Interface Summary

Interface	Description
IConstr	The most general abstraction for handling a constraint.
IGroupSolver	Represents a CNF in which clauses are grouped into levels.
ILogAble	Utility interface to catch objects with logging capability (able to log).
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.
ISolverService	The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format.
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.
RandomAccessModel	That interface allows to efficiently retrieve the truth value of a given variable in the solver.
SearchListener<S extends ISolverService>	Interface to the solver main steps.
UnitClauseProvider	Interface for engines able to derive unit clauses for the current problem.
UnitPropagationListener	Interface providing the unit propagation capability.

Class Summary

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

Exception Summary

Exception	Description
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 intended for users dealing with SAT solvers as black boxes.

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