1 2 /* 3 * File SATSolver.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file SATSolver.hpp 21 * Defines class SATSolver. 22 */ 23 24 #ifndef __SATSolver__ 25 #define __SATSolver__ 26 27 #include "SATLiteral.hpp" 28 #include "SATInference.hpp" 29 30 namespace SAT { 31 32 class SATSolver { 33 public: 34 enum VarAssignment { 35 TRUE, 36 FALSE, 37 DONT_CARE, // to represent partial models 38 NOT_KNOWN 39 }; 40 enum Status { 41 SATISFIABLE, 42 UNSATISFIABLE, 43 /** 44 * Solving for just a bounded number of conflicts may return UNKNOWN. 45 **/ 46 UNKNOWN 47 }; 48 ~SATSolver()49 virtual ~SATSolver() {} 50 51 /** 52 * Add a clause to the solver. 53 * 54 * In the clause each variable occurs at most once. (No repeated literals, no tautologies.) 55 * 56 * Memory-wise, the clause is NOT owned by the solver. Yet it shouldn't be destroyed while the solver lives. 57 * TODO: This is not ideal and should be addressed! (reference counting?) 58 */ 59 virtual void addClause(SATClause* cl) = 0; 60 addClausesIter(SATClauseIterator cit)61 void addClausesIter(SATClauseIterator cit) { 62 CALL("SATSolver::addClauses"); 63 while (cit.hasNext()) { 64 addClause(cit.next()); 65 } 66 } 67 68 /** 69 * When a solver supports partial models (via DONT_CARE values in the assignment), 70 * a partial model P computed must satisfy all the clauses added to the solver 71 * via addClause and there must be a full model extending P which also 72 * satisfies clauses added via addClauseIgnoredInPartialModel. 73 * 74 * This is a default implementation of addClauseIgnoredInPartialModel 75 * for all the solvers which return total models 76 * for which addClause and addClauseIgnoredInPartialModel 77 * naturally coincide. 78 */ addClauseIgnoredInPartialModel(SATClause * cl)79 virtual void addClauseIgnoredInPartialModel(SATClause* cl) { addClause(cl); } 80 81 /** 82 * Opportunity to perform in-processing of the clause database. 83 */ simplify()84 virtual void simplify() {} 85 86 /** 87 * Establish Status of the clause set inserted so far. 88 * 89 * If conflictCountLimit==0, 90 * do only unit propagation, if conflictCountLimit==UINT_MAX, do 91 * full satisfiability check, and for values in between, restrict 92 * the number of conflicts, and in case it is reached, stop with 93 * solving and assign the status to UNKNOWN. 94 */ 95 virtual Status solve(unsigned conflictCountLimit) = 0; 96 solve(bool onlyPropagate=false)97 Status solve(bool onlyPropagate=false) { return solve(onlyPropagate ? 0u : UINT_MAX); } 98 99 /** 100 * If status is @c SATISFIABLE, return assignment of variable @c var 101 */ 102 virtual VarAssignment getAssignment(unsigned var) = 0; 103 104 /** 105 * If status is @c SATISFIABLE, return true if the assignment of @c var is 106 * implied only by unit propagation (i.e. does not depend on any decisions) 107 */ 108 virtual bool isZeroImplied(unsigned var) = 0; 109 /** 110 * Collect zero-implied literals. 111 * 112 * Can be used in SATISFIABLE and UNKNOWN state. 113 * 114 * @see isZeroImplied() 115 */ 116 virtual void collectZeroImplied(SATLiteralStack& acc) = 0; 117 /** 118 * Return a valid clause that contains the zero-implied literal 119 * and possibly the assumptions that implied it. Return 0 if @c var 120 * was an assumption itself. 121 * If called on a proof producing solver, the clause will have 122 * a proper proof history. 123 */ 124 virtual SATClause* getZeroImpliedCertificate(unsigned var) = 0; 125 126 /** 127 * Ensure that clauses mentioning variables 1..newVarCnt can be handled. 128 * 129 * See also newVar for a different (and conceptually incompatible) 130 * way for managing variables in the solver. 131 */ ensureVarCount(unsigned newVarCnt)132 virtual void ensureVarCount(unsigned newVarCnt) {} 133 134 /** 135 * Allocate a slot for a new (previosly unused) variable in the solver 136 * and return the variable. 137 * 138 * Variables start from 1 and keep increasing by 1. 139 */ 140 virtual unsigned newVar() = 0; 141 142 virtual void suggestPolarity(unsigned var, unsigned pol) = 0; 143 144 /** 145 * Suggest random polarity for variables up to maxVar (inclusive), 146 * so that the next call to solver will tend to produce 147 * a different model (provided the status will be satisfiable). 148 */ randomizeForNextAssignment(unsigned maxVar)149 virtual void randomizeForNextAssignment(unsigned maxVar) { 150 CALL("SATSolver::randomizeForNextAssignment"); 151 for (unsigned var=1; var <= maxVar; var++) { 152 suggestPolarity(var,Random::getBit()); 153 } 154 } 155 156 /** 157 * Immediately after a call to solveXXX that returned UNSAT, 158 * this method can be used to obtain the corresponding 159 * empty SATClause as a root of a corresponding refutation tree. 160 * 161 * (However, the empty clause may be invalidated later on.) 162 */ 163 virtual SATClause* getRefutation() = 0; 164 165 /** 166 * Under the same conditions as getRefutation 167 * a solver may return a list of SAT clauses which 168 * where shown unsatisfiable 169 * (possibly under additional assumptions the caller keeps track of themselves). 170 * 171 * A solver may ignore to implement this function 172 * and will return an empty list instead. 173 */ getRefutationPremiseList()174 virtual SATClauseList* getRefutationPremiseList() { return SATClauseList::empty(); } 175 176 /** 177 * Record the association between a SATLiteral var and a Literal 178 * In TWLSolver this is used for computing niceness values 179 * 180 * TODO: an experimental hack; test it, and then either incorporate properly or remove 181 */ 182 virtual void recordSource(unsigned satlitvar, Literal* lit) = 0; 183 184 /** 185 * If status is @c SATISFIABLE, return assignment of variable @c var 186 */ trueInAssignment(SATLiteral lit)187 bool trueInAssignment(SATLiteral lit) 188 { 189 CALL("SATSolver::trueInAssignment"); 190 191 VarAssignment asgn = getAssignment(lit.var()); 192 VarAssignment desired = lit.polarity() ? TRUE : FALSE; 193 return asgn==desired; 194 } 195 196 /** 197 * If status is @c SATISFIABLE, return assignment of variable @c var 198 */ falseInAssignment(SATLiteral lit)199 bool falseInAssignment(SATLiteral lit) 200 { 201 CALL("SATSolver::trueInAssignment"); 202 203 VarAssignment asgn = getAssignment(lit.var()); 204 VarAssignment desired = lit.polarity() ? FALSE: TRUE; 205 return asgn==desired; 206 } 207 }; 208 209 class SATSolverWithAssumptions: 210 public SATSolver { 211 public: 212 213 // The first three functions represent the original TWLSolver-style of interface ... 214 215 /** 216 * Add assumption to the solver. Perhaps process partially, 217 * but mainly ensure the assumption is considered during the next calls to solve() 218 */ 219 virtual void addAssumption(SATLiteral lit) = 0; 220 221 /** 222 * Retract all the assumptions added so far. 223 * The solver becomes assumption-free. 224 * 225 * Note: this may destroy the model computed during a previous call to solve 226 * (as it currently does in TWL). 227 */ 228 virtual void retractAllAssumptions() = 0; 229 230 /** 231 * Test whether any assumptions are currently registered by the solver. 232 */ 233 virtual bool hasAssumptions() const = 0; 234 235 // ... a better alternative could be the interface below. 236 237 // It is currently implemented in terms of the one above 238 // (but may be overridden in SATSolver implementations). 239 // Note the the below interface allows the solver 240 // to identify a subset of the given assumptions that were only needed for 241 // previous contradiction to be derived. 242 243 // Note also, however, that solveUnderAssumptions cannot guarantee 244 // access to the model after it returns SATISFIABLE, as it uses retractAllAssumptions 245 // to clean in the end. 246 solveUnderAssumptions(const SATLiteralStack & assumps,unsigned conflictCountLimit,bool onlyProperSubusets)247 virtual Status solveUnderAssumptions(const SATLiteralStack& assumps, unsigned conflictCountLimit, bool onlyProperSubusets) { 248 CALL("SATSolver::solveUnderAssumptions"); 249 250 ASS(!hasAssumptions()); 251 _failedAssumptionBuffer.reset(); 252 253 Status res = solve(conflictCountLimit); 254 if (res == UNSATISFIABLE) { 255 return res; 256 } 257 258 SATLiteralStack::ConstIterator it(assumps); 259 while (it.hasNext()) { 260 SATLiteral lit = it.next(); 261 addAssumption(lit); 262 _failedAssumptionBuffer.push(lit); 263 264 res = solve(conflictCountLimit); 265 if (res == UNSATISFIABLE) { 266 break; 267 } 268 } 269 270 retractAllAssumptions(); 271 return res; 272 } 273 274 /** 275 * Solve under the given set of assumptions @b assumps. 276 * If UNSATISFIABLE is returned, a subsequent call to 277 * failedAssumptions() returns a subset of these 278 * that are already sufficient for the unsatisfiability. 279 * 280 * @b onlyPropagate suggests that a limited (and potentially incomplete) 281 * solving strategy should be employed which only performs unit propagation. 282 * 283 * If @b onlyProperSubusets, time can be saved by 284 * skipping the case when all the given assumptions 285 * would need to be considered to obtain unsatisfiability 286 * and UNKOWN can be returned instead right away. 287 */ solveUnderAssumptions(const SATLiteralStack & assumps,bool onlyPropagate=false,bool onlyProperSubusets=false)288 Status solveUnderAssumptions(const SATLiteralStack& assumps, bool onlyPropagate=false, bool onlyProperSubusets=false) { 289 return solveUnderAssumptions(assumps,onlyPropagate ? 0u : UINT_MAX,onlyProperSubusets); 290 } 291 292 /** 293 * When solveUnderAssumptions(assumps) returns UNSATISFIABLE, 294 * failedAssumptions contain a subset of assumps that is sufficient 295 * for this UNSATISFIABLE status. 296 */ failedAssumptions()297 virtual const SATLiteralStack& failedAssumptions() { 298 return _failedAssumptionBuffer; 299 } 300 301 /** 302 * Apply fixpoint minimization to already obtained failed assumption set 303 * and return the result (as failedAssumptions). 304 */ explicitlyMinimizedFailedAssumptions(bool onlyPropagate=false,bool randomize=false)305 const SATLiteralStack& explicitlyMinimizedFailedAssumptions(bool onlyPropagate=false, bool randomize = false) { 306 return explicitlyMinimizedFailedAssumptions(onlyPropagate ? 0u : UINT_MAX, randomize); 307 } 308 explicitlyMinimizedFailedAssumptions(unsigned conflictCountLimit,bool randomize)309 virtual const SATLiteralStack& explicitlyMinimizedFailedAssumptions(unsigned conflictCountLimit, bool randomize) { 310 CALL("SATSolver::explicitlyMinimizeFailedAssumptions"); 311 312 // assumes solveUnderAssumptions(...,conflictCountLimit,...) just returned UNSAT and initialized _failedAssumptionBuffer 313 314 ASS(!hasAssumptions()); 315 316 unsigned sz = _failedAssumptionBuffer.size(); 317 318 if (!sz) { // a special case. Because of the bloody unsigned (see below)! 319 return _failedAssumptionBuffer; 320 } 321 322 if (randomize) { 323 // randomly permute the content of _failedAssumptionBuffer 324 // not to bias minimization from one side or another 325 for(unsigned i=sz-1; i>0; i--) { 326 unsigned tgtPos=Random::getInteger(i+1); 327 std::swap(_failedAssumptionBuffer[i], _failedAssumptionBuffer[tgtPos]); 328 } 329 } 330 331 unsigned i = 0; 332 while (i < sz) { 333 // load all but i-th 334 for (unsigned j = 0; j < sz; j++) { 335 if (j != i) { 336 addAssumption(_failedAssumptionBuffer[j]); 337 } 338 } 339 340 if (solve(conflictCountLimit) == UNSATISFIABLE) { 341 // leave out forever by overwriting by the last one (buffer shrinks implicitly) 342 _failedAssumptionBuffer[i] = _failedAssumptionBuffer[--sz]; 343 } else { 344 // move on 345 i++; 346 } 347 348 retractAllAssumptions(); 349 } 350 351 _failedAssumptionBuffer.truncate(sz); 352 return _failedAssumptionBuffer; 353 } 354 355 protected: 356 SATLiteralStack _failedAssumptionBuffer; 357 }; 358 359 /** 360 * A convenience class for solvers which do not track actual refutations 361 * and so return the whole set of clauses added so far as refutations. 362 * 363 * This need not necessarily inherit from SATSolverWithAssumptions, 364 * but why bother with multiple inheritance if we know the only 365 * two descendants of this class will need it... 366 */ 367 class PrimitiveProofRecordingSATSolver : public SATSolverWithAssumptions { 368 public: PrimitiveProofRecordingSATSolver()369 PrimitiveProofRecordingSATSolver() : 370 _addedClauses(0), _refutation(new(0) SATClause(0)), _refutationInference(new PropInference(SATClauseList::empty())) 371 { 372 CALL("PrimitiveProofRecordingSATSolver::PrimitiveProofRecordingSATSolver"); 373 374 _refutation->setInference(_refutationInference); 375 } 376 ~PrimitiveProofRecordingSATSolver()377 virtual ~PrimitiveProofRecordingSATSolver() { 378 CALL("PrimitiveProofRecordingSATSolver::~PrimitiveProofRecordingSATSolver"); 379 380 // cannot clear the list - some inferences may be keeping its suffices till proof printing phase ... 381 // _addedClauses->destroy(); // we clear the list but not its content 382 } 383 addClause(SATClause * cl)384 virtual void addClause(SATClause* cl) override 385 { 386 CALL("PrimitiveProofRecordingSATSolver::addClause"); 387 388 SATClauseList::push(cl,_addedClauses); 389 } 390 getRefutation()391 virtual SATClause* getRefutation() override 392 { 393 CALL("PrimitiveProofRecordingSATSolver::getRefutation"); 394 395 // connect the added clauses ... 396 SATClauseList* prems = _addedClauses; 397 398 // ... with the current assumptions 399 400 // TODO: the assumption set will be empty after a call to solveUnderAssumptions() 401 // This does not matter much since refutations are only ever passed to collectFOPremises 402 // and there are no FO premises of assumption inferences 403 404 // So the below is commented out to prevent useless leaking 405 406 /* 407 for (size_t i=0; i < _assumptions.size(); i++) { 408 SATClause* unit = new(1) SATClause(1); 409 (*unit)[0] = _assumptions[i]; 410 unit->setInference(new AssumptionInference()); 411 SATClauseList::push(unit,prems); 412 } 413 */ 414 415 _refutationInference->setPremises(prems); 416 417 return _refutation; 418 } 419 getRefutationPremiseList()420 virtual SATClauseList* getRefutationPremiseList() override { 421 return _addedClauses; 422 } 423 424 private: 425 // to be used for the premises of a refutation 426 SATClauseList* _addedClauses; 427 428 /** 429 * Empty clause to be returned by the getRefutation call. 430 * Recycled between consecutive getRefutation calls. 431 */ 432 SATClause* _refutation; 433 /** 434 * The inference inside _refutation. 435 */ 436 PropInference* _refutationInference; 437 }; 438 439 440 } 441 442 #endif // __SATSolver__ 443