solver.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2012, Benjamin Kaufmann
// 
// This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
// 
// Clasp is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
// 
// Clasp is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
// 
// You should have received a copy of the GNU General Public License
// along with Clasp; if not, write to the Free Software
// Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
//
#ifndef CLASP_SOLVER_H_INCLUDED
#define CLASP_SOLVER_H_INCLUDED
#ifdef _MSC_VER
#pragma once
#pragma warning (disable : 4996) // 'std::copy': Function call with parameters that may be unsafe
#endif

#include <clasp/solver_types.h>
#include <clasp/solver_strategies.h>
#include <clasp/shared_context.h>

namespace Clasp { 

struct SearchLimits {
        explicit SearchLimits(uint64 conf = UINT64_MAX) 
                : conflicts(conf)
                , local(UINT64_MAX)
                , memLimit(UINT64_MAX)
                , dynamic(0)
                , learnts(UINT32_MAX) {
        }
        bool reached()           const { return conflicts == 0 || local == 0 || hasDynamicRestart(); }
        bool hasDynamicRestart() const { return dynamic && dynamic->isRestart(); } 
        void setMemLimit(uint32 limitInMB) { memLimit = limitInMB ? static_cast<uint64>(limitInMB)<<20 : UINT64_MAX; }
        uint64    conflicts; 
        uint64    local;     
        uint64    memLimit;  
        SumQueue* dynamic;   
        uint32    learnts;   
};



class Solver {
public:
        typedef PodVector<Constraint*>::type      ConstraintDB;
        typedef const ConstraintDB&               DBRef;
        typedef SingleOwnerPtr<DecisionHeuristic> Heuristic;
private:
        friend class SharedContext;
        Solver(SharedContext* ctx, uint32 id);
        ~Solver();
        void reset();
        void resetId(uint32 id) { strategy.id = id; }
        void startInit(uint32 constraintGuess);
        bool cloneDB(const ConstraintDB& db);
        bool preparePost();
        bool endInit();
public:
        const SharedContext*    sharedContext() const { return shared_; }
        SatPreprocessor*        satPrepro()     const;
        const SolverParams&     configuration() const;
        const SolveParams&      searchConfig()  const;
        const Heuristic&        heuristic()     const { return heuristic_;}
        uint32                  id()            const { return strategy.id; }
        Heuristic&              heuristic()           { return heuristic_;}
        VarInfo                 varInfo(Var v)  const { return shared_->validVar(v) ? shared_->varInfo(v) : VarInfo(); }
        const SymbolTable&      symbolTable()   const { return shared_->symbolTable(); }
        Literal                 tagLiteral()    const { return tag_; }

        void                    add(Constraint* c);

        bool                    add(const ClauseRep& c, bool isNew = true);
        bool                    allowImplicit(const ClauseRep& c) const {
                return c.isImp() 
                  ? shared_->allowImplicit(c.info.type()) && !c.info.aux() && (c.prep == 1 || (!auxVar(c.lits[0].var()) && !auxVar(c.lits[1].var()) && (c.size == 2 || !auxVar(c.lits[2].var()))))
                  : c.size <= 1;
        }
        PostPropagator*         getPost(uint32 prio) const;

        bool                    addPost(PostPropagator* p) { return addPost(p, initPost_ != 0); }

        void                    removePost(PostPropagator* p){ post_.remove(p); }


        ValueRep search(SearchLimits& limit, double randf = 0.0);
        ValueRep search(uint64 maxC, uint32 maxL, bool local = false, double rp  = 0.0) {
                SearchLimits limit;
                if (!local) { limit.conflicts = maxC; }
                else        { limit.conflicts = UINT64_MAX; limit.local = maxC; }
                limit.learnts = maxL;
                return search(limit, rp);
        }

        bool pushRoot(const LitVec& path);
        bool pushRoot(Literal p);
        
        void setEnumerationConstraint(Constraint* c);


        void pushRootLevel(uint32 i = 1) { 
                levels_.root      = std::min(decisionLevel(), levels_.root+i);
                levels_.backtrack = std::max(levels_.backtrack, levels_.root);
        }
        

        bool popRootLevel(uint32 i = 1, LitVec* popped = 0, bool aux = true);

        void clearStopConflict();

        uint32 rootLevel() const { return levels_.root; }


        bool clearAssumptions();

        void addLearnt(LearntConstraint* c, uint32 size, ConstraintType type) {
                learnts_.push_back(c);
                stats.addLearnt(size, type); 
        }
        void addLearnt(LearntConstraint* c, uint32 size) { addLearnt(c, size, c->type()); }

        uint32          receive(SharedLiterals** out, uint32 maxOut) const;

        SharedLiterals* distribute(const Literal* lits, uint32 size, const ClauseInfo& extra);
        

        void restart() {
                undoUntil(0);
                ++stats.restarts;
                ccInfo_.setActivity(ccInfo_.activity() + 1);
        }

        void setBacktrackLevel(uint32 dl) {
                levels_.backtrack = std::max(std::min(dl, decisionLevel()), rootLevel());
        }
        uint32 backtrackLevel() const { return levels_.backtrack; }

        bool splittable() const;


        bool split(LitVec& out);


        void copyGuidingPath(LitVec& out);


        bool simplify();
        void shuffleOnNextSimplify(){ shufSimp_ = 1; }


        Var  pushTagVar(bool pushToRoot);

        void removeConditional();
        

        void strengthenConditional();


        bool force(const Literal& p, const Antecedent& a) {
                assert(!hasConflict() || isTrue(p));
                if (assign_.assign(p, decisionLevel(), a)) return true;
                setConflict(p, a, UINT32_MAX);
                return false;
        }
        bool force(const Literal& p, const Antecedent& a, uint32 data) {
                return data != UINT32_MAX 
                        ? assign_.assign(p, decisionLevel(), a.constraint(), data) || (setConflict(p, a, data), false)
                        : force(p, a);
        }


        bool force(Literal p, uint32 dl, const Antecedent& r, uint32 d = UINT32_MAX) {
                // Correct level?
                if (dl == decisionLevel())      { return force(p, r, d); } 
                ImpliedLiteral* x = 0;
                // Already implied?
                if (isTrue(p) && (level(p.var()) <= dl || (x = impliedLits_.find(p)) != 0)) {
                        if (level(p.var()) <= dl)     { return true; }
                        if (x->level       <= dl)     { return true; }
                        *x = ImpliedLiteral(p, dl, r, d);
                        return setReason(p, r, d); // r is stronger
                }
                // Can we return to correct level?
                if (undoUntil(dl, false) == dl) { return force(p, r, d); }
                // Logically the implication is on level dl.
                // Store enough information so that p can be re-assigned once we backtrack.
                assert(!x);
                impliedLits_.add(decisionLevel(), ImpliedLiteral(p, dl, r, d));
                return (isTrue(p) && setReason(p, r, d)) || force(p, r, d);
        }
        bool force(Literal p) { return force(p, 0, Antecedent(posLit(0))); }


        bool assume(const Literal& p);


        bool decideNextBranch(double f = 0.0);


        void setStopConflict();

        bool propagate();

        bool propagateUntil(PostPropagator* p) { assert((!p || post_.active()) && "OP not allowed during init!"); return unitPropagate() && (p == post_.active() || post_.propagate(*this, p)); }


        bool test(Literal p, PostPropagator* c);


        uint32 estimateBCP(const Literal& p, int maxRecursionDepth = 5) const;


        uint32 inDegree(WeightLitVec& out);
        
        struct DBInfo { uint32 size; uint32 locked; uint32 pinned; };

        DBInfo reduceLearnts(float remMax, const ReduceStrategy& rs = ReduceStrategy());


        bool resolveConflict();


        bool backtrack();


        void undoUntil(uint32 dl);
        
        uint32 undoUntil(uint32 dl, bool popBtLevel);
        

        Var  pushAuxVar();
        void popAuxVar(uint32 num = UINT32_MAX);
        

        uint32   numProblemVars()       const { return shared_->numVars(); }
        uint32   numAuxVars()           const { return numVars() - numProblemVars(); }
        uint32   numVars()              const { return assign_.numVars() - 1; }
        bool     validVar(Var var)      const { return var <= numVars(); }
        bool     auxVar(Var var)        const { return shared_->numVars() < var; }
        uint32   numAssignedVars()      const { return assign_.assigned(); }

        uint32   numFreeVars()          const { return assign_.free()-1; }
        ValueRep value(Var v)           const { assert(validVar(v)); return assign_.value(v); }
        ValueRep topValue(Var v)        const { return level(v) == 0 ? value(v) : value_free; }
        ValueSet pref(Var v)            const { assert(validVar(v)); return assign_.pref(v);}
        bool     isTrue(Literal p)      const { assert(validVar(p.var())); return assign_.value(p.var()) == trueValue(p); }
        bool     isFalse(Literal p)     const { assert(validVar(p.var())); return assign_.value(p.var()) == falseValue(p); }

        Literal  trueLit(Var v)         const { assert(value(v) != value_free); return Literal(v, valSign(value(v))); }

        uint32   level(Var v)           const { assert(validVar(v)); return assign_.level(v); }

        bool     seen(Var v)            const { assert(validVar(v)); return assign_.seen(v, 3u); }
        bool     seen(Literal p)        const { assert(validVar(p.var())); return assign_.seen(p.var(), uint8(1+p.sign())); }
        uint32   decisionLevel()        const { return (uint32)levels_.size(); }
        bool     validLevel(uint32 dl)  const { return dl != 0 && dl <= decisionLevel(); }

        uint32   levelStart(uint32 dl)  const { assert(validLevel(dl)); return levels_[dl-1].trailPos; }

        Literal  decision(uint32 dl)    const { assert(validLevel(dl)); return assign_.trail[ levels_[dl-1].trailPos ]; }
        bool     hasConflict()          const { return !conflict_.empty(); }
        bool     hasStopConflict()      const { return hasConflict() && conflict_[0] == negLit(0); }
        uint32   queueSize()            const { return (uint32) assign_.qSize(); }
        uint32   numConstraints()       const;
        uint32   numLearntConstraints() const { return (uint32)learnts_.size(); }

        const Antecedent& reason(Literal p)              const { assert(isTrue(p)); return assign_.reason(p.var()); }
        uint32            reasonData(Literal p)          const { return assign_.data(p.var()); }

        const LitVec&     trail()                        const { return assign_.trail; }
        const Assignment& assignment()                   const { return assign_; }
        const LitVec&     conflict()                     const { return conflict_; }
        const LitVec&     conflictClause()               const { return cc_; }
        const LitVec&     symmetric()                    const { return temp_; }
        Constraint*       enumerationConstraint()        const { return enum_; }
        DBRef             constraints()                  const { return constraints_; }

        LearntConstraint& getLearnt(uint32 idx)          const {
                assert(idx < numLearntConstraints());
                return *static_cast<LearntConstraint*>(learnts_[ idx ]);
        }
        
        SolverStrategies  strategy; 
        RNG               rng;      
        ValueVec          model;    
        SolverStats       stats;    


        uint32        numWatches(Literal p)              const;
        bool          hasWatch(Literal p, Constraint* c) const;
        bool          hasWatch(Literal p, ClauseHead* c) const;

        GenericWatch* getWatch(Literal p, Constraint* c) const;

        void addWatch(Literal p, Constraint* c, uint32 data = 0) {
                assert(validWatch(p));
                watches_[p.index()].push_right(GenericWatch(c, data));
        }
        void addWatch(Literal p, const ClauseWatch& w) {
                assert(validWatch(p));
                watches_[p.index()].push_left(w);
        }

        void removeWatch(const Literal& p, Constraint* c);
        void removeWatch(const Literal& p, ClauseHead* c);

        void addUndoWatch(uint32 dl, Constraint* c) {
                assert(validLevel(dl));
                if (levels_[dl-1].undo != 0) {
                        levels_[dl-1].undo->push_back(c);
                }
                else {
                        levels_[dl-1].undo = allocUndo(c);
                }
        }
        bool removeUndoWatch(uint32 dl, Constraint* c);

        bool addPost(PostPropagator* p, bool init) { post_.add(p, p->priority()); return !init || p->init(*this); }

        bool setReason(Literal p, const Antecedent& x, uint32 data = UINT32_MAX) {
                assert(isTrue(p) || shared_->eliminated(p.var()));
                assign_.setReason(p.var(), x);
                if (data != UINT32_MAX) { assign_.setData(p.var(), data); }
                return true;
        }
        void requestData(Var v) { assign_.requestData(v + 1); }
        void setPref(Var v, ValueSet::Value which, ValueRep to) {
                assert(validVar(v) && to <= value_false);
                assign_.requestPrefs();
                assign_.setPref(v, which, to);
        }
        void reason(Literal p, LitVec& out) { assert(isTrue(p)); out.clear(); return assign_.reason(p.var()).reason(*this, p, out); }

        uint32 updateLearnt(Literal p, const Literal* first, const Literal* last, uint32 cLbd, bool forceUp = false) {
                uint32 up = strategy.updateLbd;
                if ((up || forceUp) && cLbd > 1) {
                        uint32 strict = (up == 2u);
                        uint32 p1     = (up == 3u);
                        uint32 nLbd   = (strict|p1) + countLevels(first, last, cLbd - strict);
                        if (nLbd < cLbd) { cLbd = nLbd - p1; }
                }
                if (strategy.bumpVarAct && isTrue(p)) { bumpAct_.push_back(WeightLiteral(p, cLbd)); }
                return cLbd;
        }
        bool ccMinimize(Literal p, CCMinRecursive* rec) const {
                return seen(p.var()) || 
                        (rec && hasLevel(level(p.var())) && rec->checkRecursive(p));
        }

        bool  learntLimit(const SearchLimits& x) const { return numLearntConstraints() > x.learnts || memUse_ > x.memLimit; }
        
        void* allocSmall()       { return smallAlloc_->allocate(); }
        void  freeSmall(void* m) { smallAlloc_->free(m);    }
        
        void  addLearntBytes(uint32 bytes)  { memUse_ += bytes; }
        void  freeLearntBytes(uint64 bytes) { memUse_ -= (bytes < memUse_) ? bytes : memUse_; }
        
        uint32 simplifyConflictClause(LitVec& cc, ClauseInfo& info, ClauseHead* rhs);
        uint32 finalizeConflictClause(LitVec& cc, ClauseInfo& info, uint32 ccRepMode = 0);
        uint32 countLevels(const Literal* first, const Literal* last, uint32 maxLevels);
        bool hasLevel(uint32 dl)    const { assert(validLevel(dl)); return levels_[dl-1].marked != 0; }
        bool frozenLevel(uint32 dl) const { assert(validLevel(dl)); return levels_[dl-1].freeze != 0; }
        void markLevel(uint32 dl)    { assert(validLevel(dl)); levels_[dl-1].marked = 1; }
        void freezeLevel(uint32 dl)  { assert(validLevel(dl)); levels_[dl-1].freeze = 1; }
        void unmarkLevel(uint32 dl)  { assert(validLevel(dl)); levels_[dl-1].marked = 0; }
        void unfreezeLevel(uint32 dl){ assert(validLevel(dl)); levels_[dl-1].freeze = 0; }
        void markSeen(Var v)         { assert(validVar(v)); assign_.setSeen(v, 3u); }
        void markSeen(Literal p)     { assert(validVar(p.var())); assign_.setSeen(p.var(), uint8(1+p.sign())); }
        void clearSeen(Var v)        { assert(validVar(v)); assign_.clearSeen(v);  }
private:
        struct DLevel {
                explicit DLevel(uint32 pos = 0, ConstraintDB* u = 0)
                        : trailPos(pos)
                        , marked(0)
                        , freeze(0)
                        , undo(u) {}
                uint32        trailPos : 30;
                uint32        marked   :  1;
                uint32        freeze   :  1;
                ConstraintDB* undo;
        };
        struct DecisionLevels : public PodVector<DLevel>::type {
                DecisionLevels() : root(0), backtrack(0) {}
                uint32 root;      // root level
                uint32 backtrack; // backtrack level
        };
        typedef PodVector<Antecedent>::type ReasonVec;
        typedef PodVector<WatchList>::type  Watches;
        struct PPList {
                PPList();
                ~PPList();
                void add(PostPropagator* p, uint32 prio);
                void remove(PostPropagator* p);
                bool propagate(Solver& s, PostPropagator* p) const;
                void simplify(Solver& s, bool shuf);
                void cancel()           const;
                bool isModel(Solver& s) const;
                void disable();
                void enable();
                PostPropagator* head()  const { return list; }
                PostPropagator* active()const { return *act; }
                PostPropagator* list;// head of pp-list
                PostPropagator**act; // head of active and initialized pps
        };
        struct CmpScore {
                typedef std::pair<uint32, Activity> ViewPair;
                CmpScore(const ConstraintDB& learnts, ReduceStrategy::Score sc, uint32 g) : db(learnts), rs(sc), glue(g) {}
                uint32 score(const Activity& act)                             const { return ReduceStrategy::asScore(rs, act); }
                bool operator()(uint32 lhsId, uint32 rhsId)                   const { return (*this)(db[lhsId], db[rhsId]); }
                bool operator()(const ViewPair& lhs, const ViewPair& rhs)     const { return this->operator()(lhs.second, rhs.second); }
                bool operator()(Activity lhs, Activity rhs)                   const { return ReduceStrategy::compare(rs, lhs, rhs) < 0;}
                bool operator()(const Constraint* lhs, const Constraint* rhs) const {
                        return this->operator()(
                                static_cast<const LearntConstraint*>(lhs)->activity(), 
                                static_cast<const LearntConstraint*>(rhs)->activity());
                }
                const ConstraintDB&   db;
                ReduceStrategy::Score rs;
                uint32                glue;
        private: CmpScore& operator=(const CmpScore&);
        };
        bool    validWatch(Literal p) const { return p.index() < (uint32)watches_.size(); }
        void    freeMem();
        bool    simplifySAT();
        bool    unitPropagate();
        void    cancelPropagation() { assign_.qReset(); post_.cancel(); }
        void    undoLevel(bool sp);
        uint32  analyzeConflict();
        void    otfs(Antecedent& lhs, const Antecedent& rhs, Literal p, bool final);
        ClauseHead* otfsRemove(ClauseHead* c, const LitVec* newC);
        uint32  ccMinimize(LitVec& cc, LitVec& removed, uint32 antes, CCMinRecursive* ccMin);
        bool    ccRemovable(Literal p, uint32 antes, CCMinRecursive* ccMin);
        Antecedent ccHasReverseArc(Literal p, uint32 maxLevel, uint32 maxNew);
        void    ccResolve(LitVec& cc, uint32 pos, const LitVec& reason);
        void    undoFree(ConstraintDB* x);
        void    setConflict(Literal p, const Antecedent& a, uint32 data);
        uint64  updateBranch(uint32 cfl);
        DBInfo  reduceLinear(uint32 maxR, const CmpScore& cmp);
        DBInfo  reduceSort(uint32 maxR, const CmpScore& cmp);
        DBInfo  reduceSortInPlace(uint32 maxR, const CmpScore& cmp, bool onlyPartialSort);
        ConstraintDB* allocUndo(Constraint* c);
        SharedContext*    shared_;      // initialized by master thread - otherwise read-only!
        Heuristic         heuristic_;   // active decision heuristic
        CCMinRecursive*   ccMin_;       // additional data for supporting recursive strengthen
        SmallClauseAlloc* smallAlloc_;  // allocator object for small clauses
        ConstraintDB*     undoHead_;    // free list of undo DBs
        Constraint*       enum_;        // enumeration constraint - set by enumerator
        uint64            memUse_;      // memory used by learnt constraints (estimate)
        Assignment        assign_;      // three-valued assignment.
        DecisionLevels    levels_;      // information (e.g. position in trail) on each decision level
        ConstraintDB      constraints_; // problem constraints
        ConstraintDB      learnts_;     // learnt constraints
        PPList            post_;        // (possibly empty) list of post propagators
        Watches           watches_;     // for each literal p: list of constraints watching p
        LitVec            conflict_;    // conflict-literals for later analysis
        LitVec            cc_;          // temporary: conflict clause within analyzeConflict
        LitVec            temp_;        // temporary: redundant literals in simplifyConflictClause
        WeightLitVec      bumpAct_;     // temporary: lits from current dl whose activity might get an extra bump
        VarVec            lbdStamp_;    // temporary vector for computing LBD
        VarVec            cflStamp_;    // temporary vector for computing number of conflicts in branch
        ImpliedList       impliedLits_; // lits that were asserted on current dl but are logically implied earlier
        ClauseInfo        ccInfo_;      // temporary: information about conflict clause cc_
        Literal           tag_;         // aux literal for tagging learnt constraints
        uint32            lbdTime_;     // temporary counter for computing lbd
        uint32            dbIdx_;       // position of first new problem constraint in master db 
        uint32            lastSimp_ :30;// number of top-level assignments on last call to simplify
        uint32            shufSimp_ : 1;// shuffle db on next simplify?
        uint32            initPost_ : 1;// initialize new post propagators?
};

inline bool isRevLit(const Solver& s, Literal p, uint32 maxL) {
        return s.isFalse(p) && (s.seen(p) || s.level(p.var()) < maxL);
}

template <class C>
void simplifyDB(Solver& s, C& db, bool shuffle) {
        typename C::size_type j = 0;
        for (typename C::size_type i = j, end = db.size(); i != end; ++i) {
                Constraint* c = db[i];
                if (c->simplify(s, shuffle)){ c->destroy(&s, false); }
                else                        { db[j++] = c;  }
        }
        shrinkVecTo(db, j);
}




class DecisionHeuristic {
public:
        DecisionHeuristic() {}
        virtual ~DecisionHeuristic(); 
        virtual void startInit(const Solver& /* s */) {}  

        virtual void endInit(Solver& /* s */) { }  
        
        virtual void updateVar(const Solver& /* s */, Var /* v */, uint32 /* n */) = 0;
        
        virtual void simplify(const Solver& /* s */, LitVec::size_type /* st */) { }
        
        virtual void undoUntil(const Solver& /* s */, LitVec::size_type /* st */) {}
        
        virtual void newConstraint(const Solver&, const Literal* /* first */, LitVec::size_type /* size */, ConstraintType /* t */) {}
        
        virtual void updateReason(const Solver& /* s */, const LitVec& /* lits */, Literal /* resolveLit */) {}


        virtual bool bump(const Solver& /* s */, const WeightLitVec& /* lits */, double /* adj */) { return false; }
        
        bool select(Solver& s) { return s.numFreeVars() != 0 && s.assume(doSelect(s)); }


        virtual Literal doSelect(Solver& /* s */) = 0;

        virtual Literal selectRange(Solver& /* s */, const Literal* first, const Literal* /* last */) {
                return *first;
        }
        static Literal selectLiteral(Solver& s, Var v, int signScore) {
                ValueSet prefs = s.pref(v);
                if (signScore != 0 && !prefs.has(ValueSet::user_value | ValueSet::saved_value | ValueSet::pref_value)) {
                        return Literal(v, signScore < 0); 
                }
                else if (!prefs.empty()) {
                        return Literal(v, prefs.sign());
                }
                return defaultLiteral(s, v);
        }
        static Literal defaultLiteral(Solver& s, Var v) {
                switch(s.strategy.signDef) {
                        default: // 
                        case SolverStrategies::sign_atom: return Literal(v, !s.varInfo(v).has(VarInfo::BODY));
                        case SolverStrategies::sign_no  : return posLit(v);
                        case SolverStrategies::sign_yes : return negLit(v);
                        case SolverStrategies::sign_rnd : return Literal(v, s.rng.drand() < 0.5);
                        case SolverStrategies::sign_disj: return Literal(v, !s.varInfo(v).has(VarInfo::BODY|VarInfo::DISJ));
                }
        }
private:
        DecisionHeuristic(const DecisionHeuristic&);
        DecisionHeuristic& operator=(const DecisionHeuristic&);
};

class SelectFirst : public DecisionHeuristic {
public:
        void updateVar(const Solver& /* s */, Var /* v */, uint32 /* n */) {}
private:
        Literal doSelect(Solver& s);
};

}
#endif