Logo Search packages:      
Sourcecode: sat4j version File versions

int [] org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::findModel (  )  throws TimeoutException [inline]

Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable() and model() methods, as shown in the pseudo-code: if (isSatisfiable()) { return model(); } return null;

Returns:
a model of the formula as an array of literals to satisfy, or null if no model is found
Exceptions:
TimeoutException if a model cannot be found within the given timeout.
Since:
1.7

Implements org::sat4j::specs::IProblem.

Definition at line 1297 of file Solver.java.

                                                       {
            if (isSatisfiable()) {
                  return model();
            }
            // DLB findbugs ok
            // A zero length array would mean that the formula is a tautology.
            return null;
      }


Generated by  Doxygen 1.6.0   Back to index