Logo Search packages:      
Sourcecode: sat4j version File versions

boolean org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::isSatisfiable ( IVecInt  assumps,
boolean  globalTimeout 
) throws TimeoutException [inline]

Check the satisfiability of the set of constraints contained inside the solver.

Parameters:
assumps a set of literals (represented by usual non null integers in Dimacs format).
globalTimeout whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.

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

Definition at line 1038 of file Solver.java.

References org::sat4j::minisat::core::Lbool::TRUE, and org::sat4j::minisat::core::Lbool::UNDEFINED.

                                          {
            Lbool status = Lbool.UNDEFINED;

            final int howmany = voc.nVars();
            if (mseen.length < howmany) {
                  mseen = new boolean[howmany + 1];
            }
            trail.ensure(howmany);
            trailLim.ensure(howmany);
            learnedLiterals = 0;
            order.init();
            learner.init();
            restarter.init(params);
            timebegin = System.currentTimeMillis();
            slistener.start();
            model = null; // forget about previous model
            fullmodel = null;

            // propagate constraints
            Constr confl = propagate();
            if (confl != null) {
                  analyzeAtRootLevel(confl);
                  slistener.end(Lbool.FALSE);
                  cancelUntil(0);
                  return false;
            }

            // push incremental assumptions
            for (IteratorInt iterator = assumps.iterator(); iterator.hasNext();) {
                  if (!assume(voc.getFromPool(iterator.next()))
                              || (propagate() != null)) {
                        slistener.end(Lbool.FALSE);
                        cancelUntil(0);
                        return false;
                  }
            }
            rootLevel = decisionLevel();

            final long memorybound = Runtime.getRuntime().freeMemory() / 10;

            ConflictTimer freeMem = new ConflictTimerAdapter(500) {
                  private static final long serialVersionUID = 1L;

                  @Override
                  void run() {
                        long freemem = Runtime.getRuntime().freeMemory();
                        // System.out.println("c Free memory "+freemem);
                        if (freemem < memorybound) {
                              // Reduce the set of learnt clauses
                              needToReduceDB = true;
                        }
                  }
            };

            if (timeBasedTimeout) {
                  if (!global || timer == null) {
                        TimerTask stopMe = new TimerTask() {
                              @Override
                              public void run() {
                                    undertimeout = false;
                              }
                        };
                        timer = new Timer(true);
                        timer.schedule(stopMe, timeout);
                        conflictCount = freeMem;
                  }
            } else {
                  if (!global || conflictCount == null) {
                        ConflictTimer conflictTimeout = new ConflictTimerAdapter(
                                    (int) timeout) {
                              private static final long serialVersionUID = 1L;

                              @Override
                              public void run() {
                                    undertimeout = false;
                              }
                        };
                        conflictCount = new ConflictTimerContainer().add(
                                    conflictTimeout).add(freeMem);
                  }
            }
            needToReduceDB = false;
            undertimeout = true;

            // Solve
            while ((status == Lbool.UNDEFINED) && undertimeout) {
                  status = search(restarter.nextRestartNumberOfConflict());
                  // System.out.println("c speed
                  // "+(stats.decisions/((System.currentTimeMillis()-timebegin)/1000))+"
                  // dec/s, "+stats.starts+"/"+stats.conflicts);
                  restarter.onRestart();
            }

            cancelUntil(0);
            if (!global && timeBasedTimeout) {
                  timer.cancel();
                  timer = null;
            }
            slistener.end(status);
            if (!undertimeout) {
                  throw new TimeoutException(" Timeout (" + timeout + "s) exceeded"); //$NON-NLS-1$//$NON-NLS-2$
            }
            return status == Lbool.TRUE;
      }


Generated by  Doxygen 1.6.0   Back to index