1 // 2 // Copyright (c) 2006-2017 Benjamin Kaufmann 3 // 4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 5 // 6 // Permission is hereby granted, free of charge, to any person obtaining a copy 7 // of this software and associated documentation files (the "Software"), to 8 // deal in the Software without restriction, including without limitation the 9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 10 // sell copies of the Software, and to permit persons to whom the Software is 11 // furnished to do so, subject to the following conditions: 12 // 13 // The above copyright notice and this permission notice shall be included in 14 // all copies or substantial portions of the Software. 15 // 16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 22 // IN THE SOFTWARE. 23 // 24 #ifndef CLASP_ENUMERATOR_H_INCLUDED 25 #define CLASP_ENUMERATOR_H_INCLUDED 26 27 #ifdef _MSC_VER 28 #pragma once 29 #endif 30 #include <clasp/literal.h> 31 #include <clasp/constraint.h> 32 #include <clasp/minimize_constraint.h> 33 #include <clasp/util/misc_types.h> 34 35 namespace Clasp { 36 class Solver; 37 class SharedContext; 38 class Enumerator; 39 class EnumerationConstraint; 40 41 //! Type for storing a model. 42 struct Model { 43 enum Type { Sat = 0u, Brave = 1u, Cautious = 2u, User = 4u }; 44 enum { cons_mask = 3u, est_pos_mask= 4u, est_neg_mask = 8u }; estMaskModel45 static uint8 estMask(Literal p) { return est_pos_mask << ((int)p.sign()); } hasVarModel46 bool hasVar(Var v) const { return values && v < values->size(); } 47 //! True if this model stores current (cautious/brave) consequences. consequencesModel48 bool consequences() const { return (type & cons_mask) != 0; } 49 //! For sat models, value of v in model. Otherwise, undefined. valueModel50 ValueRep value(Var v) const { assert(hasVar(v)); return (*values)[v] & 3u; } 51 //! True if p is true in model or part of current consequences. isTrueModel52 bool isTrue(Literal p) const { return (value(p.var()) & trueValue(p)) != 0; } 53 //! True if p is part of a definite answer. isDefModel54 bool isDef(Literal p) const { return isTrue(p) && (def || ((type & Cautious) == 0u) || !isEst(p)); } 55 //! True if p is part of the current estimate of consequences. isEstModel56 bool isEst(Literal p) const { assert(hasVar(p.var())); return ((*values)[p.var()] & estMask(p)) != 0; } 57 void reset(); 58 uint64 num; // running number of this model 59 const Enumerator* ctx; // ctx in which model was found 60 const ValueVec* values; // variable assignment or consequences 61 const SumVec* costs; // associated costs (or 0) 62 uint32 sId :16;// id of solver that found the model 63 uint32 type:12;// type of model 64 uint32 opt : 1;// whether the model is optimal w.r.t costs (0: unknown) 65 uint32 def : 1;// whether the model is definite w.r.t consequences (0: unknown) 66 uint32 sym : 1;// whether symmetric models are possible 67 uint32 up : 1;// whether the model was updated on last unsat 68 }; 69 70 /** 71 * \defgroup enumerator Solving 72 * \brief Enumerators and solve algorithms. 73 */ 74 //@{ 75 76 //! Options for configuring enumeration. 77 struct EnumOptions { 78 typedef MinimizeMode OptMode; 79 typedef ProjectMode ProjMode; 80 enum EnumType { enum_auto = 0, enum_bt = 1, enum_record = 2, enum_dom_record = 3, enum_consequences = 4, enum_brave = 5, enum_cautious = 6, enum_query = 7, enum_user = 8 }; EnumOptionsEnumOptions81 EnumOptions() : numModels(-1), enumMode(enum_auto), optMode(MinimizeMode_t::optimize), proMode(ProjectMode_t::Implicit), project(0) {} 82 static Enumerator* createModelEnumerator(const EnumOptions& opts); 83 static Enumerator* createConsEnumerator(const EnumOptions& opts); 84 static Enumerator* nullEnumerator(); 85 static Enumerator* createEnumerator(const EnumOptions& opts); consequencesEnumOptions86 bool consequences() const { return (enumMode & enum_consequences) != 0; } modelsEnumOptions87 bool models() const { return (enumMode < enum_consequences); } optimizeEnumOptions88 bool optimize() const { return ((optMode & MinimizeMode_t::optimize) != 0); } 89 int64 numModels; /*!< Number of models to compute. */ 90 EnumType enumMode; /*!< Enumeration type to use. */ 91 OptMode optMode; /*!< Optimization mode to use. */ 92 ProjMode proMode; /*!< Projection mode to use. */ 93 uint32 project; /*!< Options for projection. */ 94 SumVec optBound; /*!< Initial bound for optimize statements. */ 95 }; 96 const char* modelType(const Model& m); 97 98 99 //! Interface for supporting enumeration of models. 100 /*! 101 * Enumerators are global w.r.t a solve algorithm. That is, 102 * even if the solve algorithm itself uses a parallel search, there 103 * shall be only one enumerator and it is the user's responsibility 104 * to protect the enumerator with appropriate locking. 105 * 106 * Concrete enumerators must implement a function for preparing a problem for enumeration 107 * and an EnumerationConstraint to be added to each solver attached to the problem. 108 * It is then the job of the actual solve algorithm to commit models to the enumerator 109 * and to integrate new information into attached solvers via appropriate calls to 110 * Enumerator::update(). 111 */ 112 class Enumerator { 113 public: 114 typedef EnumerationConstraint* ConPtr; 115 typedef EnumerationConstraint& ConRef; 116 typedef const SharedMinimizeData* Minimizer; 117 typedef EnumOptions::OptMode OptMode; 118 class ThreadQueue; 119 explicit Enumerator(); 120 virtual ~Enumerator(); 121 122 void reset(); 123 124 //! Prepares the problem for enumeration. 125 /*! 126 * The function shall be called once before search is started and before SharedContext::endInit() 127 * was called. It freezes enumeration-related variables and adds a suitable enumeration constraint 128 * to the master solver. 129 * 130 * \pre The problem is not yet frozen, i.e. SharedContext::endInit() was not yet called. 131 * \param problem The problem on which this enumerator should work. 132 * \param opt Minimization mode to apply during enumeration. 133 * \param limit Optional hint on max number of models to compute. 134 * 135 * \note In the incremental setting, init() must be called once for each incremental step. 136 */ 137 int init(SharedContext& problem, OptMode opt = MinimizeMode_t::optimize, int limit = 0); 138 139 //! Prepares the given solver for enumeration under the given path. 140 /*! 141 * The function shall be called once before solving is started. It pushes the 142 * given path to the solver by calling Solver::pushRoot() and prepares s for 143 * enumeration/optimization. 144 * \return true if path was added. 145 */ 146 bool start(Solver& s, const LitVec& path = LitVec(), bool disjointPath = false) const; 147 148 //! Updates the given solver with enumeration-related information. 149 /*! 150 * The function is used to integrate enumeration-related information, 151 * like minimization bounds or previously committed models, into the search space of s. 152 * It shall be called after each commit. 153 * 154 * \param s The solver to update. 155 * \note The function is concurrency-safe, i.e. can be called 156 * concurrently by different solvers. 157 */ 158 bool update(Solver& s) const; 159 160 /*! 161 * \name Commit functions 162 * Functions for committing enumeration-related information to the enumerator. 163 * \note The functions in this group are *not* concurrency-safe, i.e. in a parallel search 164 * at most one solver shall call a commit function at any one time. 165 */ 166 //@{ 167 168 //! Commits the model stored in the given solver. 169 /*! 170 * If the model is valid and unique, the function returns true and the 171 * model can be accessed via a call to Enumerator::lastModel(). 172 * Otherwise, the function returns false. 173 * In either case, Enumerator::update(s) shall be called 174 * in order to continue search for further models. 175 * 176 * \pre The solver's assignment is total. 177 */ 178 bool commitModel(Solver& s); 179 //! Expands the next symmetric model if any. 180 bool commitSymmetric(Solver& s); 181 //! Commits an unsatisfiable path stored in the given solver. 182 /*! 183 * The return value determines how search should proceed. 184 * If true is returned, the enumerator has relaxed an enumeration constraint 185 * and search may continue after a call to Enumerator::update(s). 186 * Otherwise, the search shall be stopped. 187 */ 188 bool commitUnsat(Solver& s); 189 //! Commits the given clause to this enumerator. 190 bool commitClause(const LitVec& clause) const; 191 //! Marks current enumeration phase as completed. 192 /*! 193 * If the enumerator was initialized with a minimization constraint and 194 * optimization mode MinimizeMode_t::enumOpt, the optimal bound is committed, 195 * the enumerator is prepared for enumerating optimal models, and the function 196 * returns false. Otherwise, the function returns true and search shall be stopped. 197 */ 198 bool commitComplete(); 199 //! Commits the state stored in the given solver. 200 /*! 201 * Calls commitModel() or commitUnsat() depending on the state of s. 202 * The function returns value_true, to signal that s stores a valid and 203 * unique model, value_false to signal that search shall be stopped, and 204 * value_free otherwise. 205 * \see commitModel() 206 * \see commitUnsat() 207 */ 208 uint8 commit(Solver& s); 209 //@} 210 211 //! Removes from s the path that was passed to start() and any active (minimization) bound. 212 void end(Solver& s) const; 213 //! Returns the number of models enumerated so far. enumerated()214 uint64 enumerated() const { return model_.num; } 215 //! Returns the last model enumerated. 216 /*! 217 * \note If enumerated() is equal to 0, the returned object is in an indeterminate state. 218 */ lastModel()219 const Model& lastModel() const { return model_; } 220 //! Returns whether optimization is active. optimize()221 bool optimize() const { return mini_ && mini_->mode() != MinimizeMode_t::enumerate && model_.opt == 0; } 222 //! Returns whether computed models are still tentative. tentative()223 bool tentative() const { return mini_ && mini_->mode() == MinimizeMode_t::enumOpt && model_.opt == 0; } 224 //! Returns the active minimization constraint if any. minimizer()225 Minimizer minimizer() const { return mini_; } 226 //! Returns the type of models this enumerator computes. modelType()227 virtual int modelType() const { return Model::Sat; } 228 enum UnsatType { 229 unsat_stop = 0u, /*!< First unsat stops search - commitUnsat() always return false. */ 230 unsat_cont = 1u, /*!< Unsat may be tentative - commitUnsat() may return true. */ 231 unsat_sync = 3u, /*!< Similar to unsat_cont but additionally requires synchronization among threads. */ 232 }; 233 //! Returns whether unsat may be tentative and/or requires synchronization. 234 virtual int unsatType() const; 235 //! Returns whether or not this enumerator supports full restarts once a model was found. supportsRestarts()236 virtual bool supportsRestarts() const { return true; } 237 //! Returns whether or not this enumerator supports parallel search. supportsParallel()238 virtual bool supportsParallel() const { return true; } 239 //! Returns whether or not this enumerator supports splitting-based search. 240 virtual bool supportsSplitting(const SharedContext& problem) const; 241 //! Returns whether this enumerator requires exhaustive search to produce a definite answer. exhaustive()242 virtual bool exhaustive() const { return mini_ && mini_->mode() != MinimizeMode_t::enumerate; } 243 //! Sets whether the search path stored in s is disjoint from all others. 244 void setDisjoint(Solver& s, bool b) const; 245 //! Sets whether symmetric should be ignored. 246 void setIgnoreSymmetric(bool b); 247 ConPtr constraint(const Solver& s) const; 248 protected: 249 //! Shall prepare the enumerator and freeze any enumeration-related variable. 250 /*! 251 * \return A prototypical enumeration constraint to be used in a solver. 252 */ 253 virtual ConPtr doInit(SharedContext& ctx, SharedMinimizeData* min, int numModels) = 0; 254 virtual void doReset(); 255 Model& model(); 256 private: 257 class SharedQueue; 258 Enumerator(const Enumerator&); 259 Enumerator& operator=(const Enumerator&); 260 ConRef constraintRef(const Solver& s) const; 261 SharedMinimizeData* mini_; 262 SharedQueue* queue_; 263 SumVec costs_; 264 Model model_; 265 }; 266 267 //! A solver-local (i.e. thread-local) constraint to support enumeration. 268 /*! 269 * An enumeration constraint is used to extract/store enumeration-related information 270 * from models. 271 */ 272 class EnumerationConstraint : public Constraint { 273 public: 274 typedef EnumerationConstraint* ConPtr; 275 typedef MinimizeConstraint* MinPtr; 276 typedef Enumerator::ThreadQueue* QueuePtr; 277 //! Returns true if search-path is disjoint from all others. disjointPath()278 bool disjointPath()const { return disjoint_; } state()279 ValueRep state() const { return state_; } resetMode()280 ValueRep resetMode() const { return upMode_; } 281 //! Returns true if optimization is active. 282 bool optimize() const; minimizer()283 MinPtr minimizer() const { return mini_; } 284 // Methods used by enumerator 285 void init(Solver& s, SharedMinimizeData* min, QueuePtr q); 286 bool start(Solver& s, const LitVec& path, bool disjoint); 287 void end(Solver& s); 288 bool update(Solver& s); 289 void setDisjoint(bool x); 290 bool integrateBound(Solver& s); 291 bool integrateNogoods(Solver& s); 292 bool commitModel(Enumerator& ctx, Solver& s); 293 bool commitUnsat(Enumerator& ctx, Solver& s); setMinimizer(MinPtr min)294 void setMinimizer(MinPtr min) { mini_ = min; } 295 void add(Constraint* c); 296 void modelHeuristic(Solver& s); 297 protected: 298 EnumerationConstraint(); 299 virtual ~EnumerationConstraint(); 300 // base interface 301 virtual void destroy(Solver* s, bool detach); propagate(Solver &,Literal,uint32 &)302 virtual PropResult propagate(Solver&, Literal, uint32&) { return PropResult(true, true); } reason(Solver &,Literal,LitVec &)303 virtual void reason(Solver&, Literal, LitVec&) {} 304 virtual bool simplify(Solver& s, bool reinit); 305 virtual bool valid(Solver& s); 306 virtual Constraint* cloneAttach(Solver& s); 307 // own interface 308 virtual ConPtr clone() = 0; 309 virtual bool doUpdate(Solver& s) = 0; doCommitModel(Enumerator &,Solver &)310 virtual void doCommitModel(Enumerator&, Solver&) {} doCommitUnsat(Enumerator &,Solver &)311 virtual void doCommitUnsat(Enumerator&, Solver&) {} rootLevel()312 uint32 rootLevel() const { return root_; } 313 private: 314 typedef PodVector<Constraint*>::type ConstraintDB; 315 typedef SingleOwnerPtr<Enumerator::ThreadQueue> QPtr; 316 MinimizeConstraint* mini_; 317 QPtr queue_; 318 ConstraintDB nogoods_; 319 LitVec next_; 320 uint32 root_; 321 ValueRep state_; 322 ValueRep upMode_; 323 ValueRep heuristic_; 324 bool disjoint_; 325 }; 326 //@} 327 } 328 329 #endif 330