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

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2