dpllt_basic.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file dpllt_basic.cpp
00004  *\brief Basic implementation of dpllt module using generic sat solver
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Mon Dec 12 19:09:43 2005
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include "dpllt_basic.h"
00023 #include "cnf.h"
00024 #include "sat_api.h"
00025 #include "exception.h"
00026 
00027 
00028 using namespace std;
00029 using namespace CVC3;
00030 using namespace SAT;
00031 
00032 
00033 //int level_ = 0;
00034 
00035 static void SATDLevelHook(void *cookie, int change)
00036 {
00037   //cout << "backtrack to: " << level_ << " " << change << endl;
00038   //level_ += change;
00039   //  cout<<"decision level called"<<endl;
00040   DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00041   for (; change > 0; change--) {
00042     db->theoryAPI()->push();
00043   }
00044   for (; change < 0; change++) {
00045     db->theoryAPI()->pop();
00046   }
00047 }
00048 
00049 
00050 static SatSolver::Lit SATDecisionHook(void *cookie, bool *done)
00051 {
00052   // cout<<"sat decision called"<<endl;
00053   DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00054 
00055   if (db->theoryAPI()->outOfResources()) {
00056     // Tell SAT solver to exit with satisfiable result
00057     *done = true;
00058     return SatSolver::Lit();
00059   }
00060 
00061   decide:
00062   if (!db->decider()) {
00063     // Tell SAT solver to make its own choice
00064     if (!*done) return SatSolver::Lit();
00065   }
00066   else {
00067     Lit lit = db->decider()->makeDecision();
00068     if (!lit.isNull()) {
00069       //cout << "Split: " << lit.getVar().getIndex() << endl;
00070       // Tell SAT solver which literal to split on
00071       *done = false;
00072       return db->cvc2SAT(lit);
00073     }
00074   }
00075 
00076   Clause c;
00077   DPLLT::ConsistentResult result;
00078   result = db->theoryAPI()->checkConsistent(c, true);
00079 
00080   if (result == DPLLT::MAYBE_CONSISTENT) {
00081     CNF_Formula_Impl cnf;
00082     bool added = db->theoryAPI()->getNewClauses(cnf);
00083     db->addNewClauses(cnf);
00084     if (!added) goto decide;
00085     // Fall through: SAT solver will continue because clauses have been added
00086   }
00087   else if (result == DPLLT::INCONSISTENT) {
00088     db->addNewClause(c);
00089   }
00090 
00091   // Tell SAT solver that we are done
00092   *done = true;
00093   return SatSolver::Lit();
00094 }
00095 
00096 
00097 static void SATAssignmentHook(void *cookie, SatSolver::Var var, int value)
00098 {
00099   //  cout<<"assignment called"<<endl;
00100   DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00101   TRACE("DPLL Assign", var.id, " := ", value);
00102   if (value == 0)
00103     db->theoryAPI()->assertLit(Lit(db->satSolver()->GetVarIndex(var), false));
00104   else if (value == 1)
00105     db->theoryAPI()->assertLit(Lit(db->satSolver()->GetVarIndex(var), true));
00106   else return;
00107   Clause c;
00108   DPLLT::ConsistentResult result;
00109   result = db->theoryAPI()->checkConsistent(c, false);
00110   if (result == DPLLT::INCONSISTENT) {
00111     db->addNewClause(c);
00112   }
00113 }
00114 
00115 
00116 static void SATDeductionHook(void *cookie)
00117 {
00118   //  cout<<"deduction called"<<endl;;
00119   DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00120   Clause c;
00121   CNF_Formula_Impl cnf;
00122   if (db->theoryAPI()->getNewClauses(cnf))
00123     db->addNewClauses(cnf);
00124   Lit l = db->theoryAPI()->getImplication();
00125   while (!l.isNull()) {
00126     db->theoryAPI()->getExplanation(l, c);
00127     db->addNewClause(c);
00128     c.clear();
00129     l = db->theoryAPI()->getImplication();
00130   }
00131 }
00132 
00133 
00134 void DPLLTBasic::createManager()
00135 {
00136   d_mng = SatSolver::Create();
00137   d_mng->RegisterDLevelHook(SATDLevelHook, this);
00138   d_mng->RegisterDecisionHook(SATDecisionHook, this);
00139   d_mng->RegisterAssignmentHook(SATAssignmentHook, this);
00140   d_mng->RegisterDeductionHook(SATDeductionHook, this);
00141 }
00142 
00143 
00144 void DPLLTBasic::generate_CDB (CNF_Formula_Impl& cnf)
00145 {
00146   CNF_Formula::const_iterator i, iend;
00147   Clause::const_iterator j, jend;
00148   vector<SatSolver::Lit> clause;
00149   if (cnf.numVars() > unsigned(d_mng->NumVariables())) {
00150     d_mng->AddVariables(cnf.numVars() - d_mng->NumVariables());
00151   }
00152   cnf.simplify();
00153   for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00154     //for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
00155     if ((*i).isSatisfied()) continue;
00156     for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
00157       if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
00158     }
00159     if (clause.size() != 0) {
00160       d_mng->AddClause(clause);
00161       clause.clear();
00162     }
00163   }
00164 }
00165 
00166 
00167 void DPLLTBasic::handle_result(SatSolver::SATStatus outcome)
00168 {
00169   char * result = "UNKNOWN";
00170   switch (outcome) {
00171     case SatSolver::SATISFIABLE:
00172 //         if (d_printStats) {
00173 //           cout << "Instance satisfiable" << endl;
00174 //           for (int i=1, sz = d_mng->NumVariables(); i <= sz; ++i) {
00175 //             switch(d_mng->GetVarAssignment(d_mng->GetVar(i))) {
00176 //               case -1:
00177 //                 cout <<"("<< i<<")"; break;
00178 //               case 0:
00179 //                 cout << "-" << i; break;
00180 //               case 1:
00181 //                 cout << i ; break;
00182 //               default:
00183 //                 throw Exception("Unknown variable value state");
00184 //      }
00185 //             cout << " ";
00186 //           }
00187 //           cout << endl;
00188 //         }
00189   result = "SAT";
00190   break;
00191     case SatSolver::UNSATISFIABLE:
00192   result  = "UNSAT";
00193         if (d_printStats) cout << "Instance unsatisfiable" << endl;
00194   break;
00195     case SatSolver::BUDGET_EXCEEDED:
00196   result  = "ABORT : TIME OUT"; 
00197   cout << "Time out, unable to determine the satisfiablility of the instance";
00198   cout << endl;
00199   break;
00200     case SatSolver::OUT_OF_MEMORY:
00201   result  = "ABORT : MEM OUT"; 
00202   cout << "Memory out, unable to determing the satisfiablility of the instance";
00203   cout << endl;
00204   break;
00205     default:
00206       throw Exception("DPLTBasic::handle_result: Unknown outcome");
00207   }
00208   if (d_printStats) d_mng->PrintStatistics();
00209 }
00210 
00211 
00212 void DPLLTBasic::verify_solution()
00213 {
00214   // Used to check that all clauses are true, but our decision maker
00215   // may ignore some clauses that are no longer relevant, so now we check to
00216   // make sure no clause is false.
00217   for (SatSolver::Clause cl = d_mng->GetFirstClause(); !cl.IsNull();
00218        cl = d_mng->GetNextClause(cl)) {
00219     vector<SatSolver::Lit> lits;
00220     d_mng->GetClauseLits(cl, &lits);
00221     for (; lits.size() != 0;) {
00222       SatSolver::Lit lit = lits.back();
00223       SatSolver::Var var = d_mng->GetVarFromLit(lit);
00224       int sign = d_mng->GetPhaseFromLit(lit);
00225       int var_value = d_mng->GetVarAssignment(var);
00226       if( (var_value == 1 && sign == 0) ||
00227     (var_value == 0 && sign == 1) ||
00228           (var_value == -1) ) break;
00229       lits.pop_back();
00230     }
00231     DebugAssert(lits.size() != 0, "DPLLTBasic::verify_solution failed");
00232   }
00233 }
00234 
00235 
00236 DPLLTBasic::DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider, ContextManager* cm,
00237                        bool printStats)
00238   : DPLLT(theoryAPI, decider), d_cm(cm), d_ready(true), 
00239     d_printStats(printStats),
00240     d_pushLevel(cm->getCurrentContext(), 0),
00241     d_readyPrev(cm->getCurrentContext(), true),
00242     d_prevStackSize(cm->getCurrentContext(), 0),
00243     d_prevAStackSize(cm->getCurrentContext(), 0)
00244 {
00245   createManager();
00246   d_cnf = new CNF_Formula_Impl();
00247   d_assertions = new CD_CNF_Formula(d_cm->getCurrentContext());
00248 }
00249 
00250 
00251 DPLLTBasic::~DPLLTBasic()
00252 {
00253   if (d_assertions) delete d_assertions;
00254   if (d_cnf) delete d_cnf;
00255   if (d_mng) delete d_mng;
00256   while (d_assertionsStack.size() > 0) {
00257     d_assertions = d_assertionsStack.back();
00258     d_assertionsStack.pop_back();
00259     delete d_assertions;
00260   }
00261   while (d_mngStack.size() > 0) {
00262     d_mng = d_mngStack.back();
00263     d_mngStack.pop_back();
00264     delete d_mng;
00265     d_cnf = d_cnfStack.back();
00266     d_cnfStack.pop_back();
00267     delete d_cnf;
00268   }
00269 }
00270 
00271 
00272 void DPLLTBasic::addNewClause(const Clause& c)
00273 {
00274   DebugAssert(c.size() > 0, "Expected non-empty clause");
00275   DebugAssert(c.getMaxVar() <= unsigned(d_mng->NumVariables()),
00276               "Expected no new variables");
00277   vector<SatSolver::Lit> lits;
00278   for (Clause::const_iterator i = c.begin(), iend = c.end(); i < iend; ++i) {
00279     if (!(*i).isFalse()) lits.push_back(cvc2SAT(*i));
00280   }
00281   satSolver()->AddClause(lits);
00282   (*d_cnf) += c;
00283 }
00284 
00285 
00286 void DPLLTBasic::addNewClauses(CNF_Formula_Impl& cnf)
00287 {
00288   CNF_Formula::const_iterator i, iend;
00289   Clause::const_iterator j, jend;
00290   vector<SatSolver::Lit> clause;
00291   if (cnf.numVars() > unsigned(d_mng->NumVariables())) {
00292     d_mng->AddVariables(cnf.numVars() - d_mng->NumVariables());
00293   }
00294   cnf.simplify();
00295   for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00296     //for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
00297     if ((*i).isSatisfied()) continue;
00298     for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
00299       if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
00300     }
00301     if (clause.size() != 0) {
00302       d_mng->AddClause(clause);
00303       clause.clear();
00304     }
00305   }
00306   generate_CDB(cnf);
00307   (*d_cnf) += cnf;
00308 }
00309 
00310 
00311 void DPLLTBasic::push()
00312 {
00313   d_theoryAPI->push();
00314   d_pushLevel = d_pushLevel + 1;
00315   d_prevStackSize = d_mngStack.size();
00316   d_prevAStackSize = d_assertionsStack.size();
00317   d_readyPrev = d_ready;
00318 }
00319 
00320 
00321 void DPLLTBasic::pop()
00322 {
00323   unsigned pushLevel = d_pushLevel;
00324   unsigned prevStackSize = d_prevStackSize;
00325   unsigned prevAStackSize = d_prevAStackSize;
00326   bool readyPrev = d_readyPrev;
00327 
00328   while (d_assertionsStack.size() > prevAStackSize) {
00329     delete d_assertions;
00330     d_assertions = d_assertionsStack.back();
00331     d_assertionsStack.pop_back();
00332   }
00333 
00334   while (d_mngStack.size() > prevStackSize) {
00335     delete d_mng;
00336     delete d_cnf;
00337     d_mng = d_mngStack.back();
00338     d_mngStack.pop_back();
00339     d_cnf = d_cnfStack.back();
00340     d_cnfStack.pop_back();
00341     DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00342   }    
00343 
00344   if (d_mngStack.size() == 0) {
00345     if (readyPrev && !d_ready) {
00346       delete d_mng;
00347       delete d_cnf;
00348       createManager();
00349       d_cnf = new CNF_Formula_Impl();
00350       d_ready = true;
00351     }
00352     else {
00353       DebugAssert(readyPrev == d_ready, "Unexpected ready values");
00354     }
00355   }
00356   else {
00357     DebugAssert(!d_ready, "Expected ready to be false");
00358   }
00359 
00360   while (d_pushLevel == pushLevel)
00361     d_theoryAPI->pop();
00362 
00363 }
00364 
00365 
00366 void DPLLTBasic::addAssertion(const CNF_Formula& cnf)
00367 {
00368   // Immediately assert unit clauses
00369   CNF_Formula::const_iterator i, iend;
00370   Clause::const_iterator j, jend;
00371   for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00372     if ((*i).isUnit()) {
00373       j = (*i).begin();
00374       d_theoryAPI->assertLit(*j);
00375     }
00376   }
00377 
00378   // Accumulate assertions in d_assertions
00379   (*d_assertions) += cnf;
00380 }
00381 
00382 
00383 QueryResult DPLLTBasic::checkSat(const CNF_Formula& cnf)
00384 {
00385   SatSolver::SATStatus result;
00386 
00387   if (!d_ready) {
00388     // Copy current formula
00389     d_cnfStack.push_back(d_cnf);
00390     d_cnf = new CNF_Formula_Impl(*d_cnf);
00391 
00392     // make unit clauses for current assignment
00393     int value;
00394     for (int i = 1; i <= d_mng->NumVariables(); ++i) {
00395       value = d_mng->GetVarAssignment(d_mng->GetVar(i));
00396       if (value == 1) {
00397         d_cnf->newClause();
00398         d_cnf->addLiteral(Lit(i));
00399       }
00400       else if (value == 0) {
00401         d_cnf->newClause();
00402         d_cnf->addLiteral(Lit(i, false));
00403       }
00404     }
00405 
00406     // Create new manager
00407     d_mngStack.push_back(d_mng);
00408     DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00409     createManager();
00410   }
00411   d_ready = false;
00412 
00413   if (d_assertions) (*d_cnf) += (*d_assertions);
00414 
00415   (*d_cnf) += cnf;
00416   generate_CDB(*d_cnf);
00417 
00418   d_theoryAPI->push();
00419 
00420   result = d_mng->Satisfiable(true);
00421   if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources())
00422     result = SatSolver::BUDGET_EXCEEDED;
00423 
00424   // Print result
00425 
00426   if (result == SatSolver::SATISFIABLE) {
00427     verify_solution();
00428     if (d_assertions->numClauses() > 0) {
00429       d_assertionsStack.push_back(d_assertions);
00430       d_assertions = new CD_CNF_Formula(d_cm->getCurrentContext());
00431     }
00432   }
00433   handle_result (result);
00434 
00435   if (result == SatSolver::UNSATISFIABLE) {
00436     d_theoryAPI->pop();
00437     delete d_mng;
00438     delete d_cnf;
00439     if (d_mngStack.size() == 0) {
00440       createManager();
00441       d_cnf = new CNF_Formula_Impl();
00442       d_ready = true;
00443     }
00444     else {
00445       d_mng = d_mngStack.back();
00446       d_mngStack.pop_back();
00447       d_cnf = d_cnfStack.back();
00448       d_cnfStack.pop_back();
00449       DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00450     }
00451   }
00452 
00453   return (result == SatSolver::UNSATISFIABLE ? UNSATISFIABLE :
00454           result == SatSolver::SATISFIABLE ? SATISFIABLE :
00455           ABORT);
00456 }
00457 
00458 
00459 QueryResult DPLLTBasic::continueCheck(const CNF_Formula& cnf)
00460 {
00461   SatSolver::SATStatus result;
00462 
00463   if (d_ready) {
00464     throw Exception
00465       ("continueCheck should be called after a previous satisfiable result");
00466   }
00467   if (d_assertions->numClauses() > 0) {
00468     throw Exception
00469       ("a check cannot be continued if new assertions have been made");
00470   }
00471   CNF_Formula_Impl cnfImpl(cnf);
00472 
00473   generate_CDB(cnfImpl);
00474   (*d_cnf) += cnfImpl;
00475 
00476   result = d_mng->Continue();
00477   if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources())
00478     result = SatSolver::BUDGET_EXCEEDED;
00479 
00480   // Print result
00481 
00482   if (result == SatSolver::SATISFIABLE)
00483     verify_solution();
00484   handle_result (result);
00485 
00486   if (result == SatSolver::UNSATISFIABLE) {
00487     d_theoryAPI->pop();
00488     delete d_mng;
00489     delete d_cnf;
00490     if (d_mngStack.size() == 0) {
00491       createManager();
00492       d_cnf = new CNF_Formula_Impl();
00493       d_ready = true;
00494     }
00495     else {
00496       d_mng = d_mngStack.back();
00497       d_mngStack.pop_back();
00498       d_cnf = d_cnfStack.back();
00499       d_cnfStack.pop_back();
00500       DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00501     }
00502   }
00503 
00504   return (result == SatSolver::UNSATISFIABLE ? UNSATISFIABLE :
00505           result == SatSolver::SATISFIABLE ? SATISFIABLE :
00506           ABORT);
00507 }

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1