minimize_constraint.h

Go to the documentation of this file.

// 
// Copyright (c) 2010-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_MINIMIZE_CONSTRAINT_H_INCLUDED
#define CLASP_MINIMIZE_CONSTRAINT_H_INCLUDED

#ifdef _MSC_VER
#pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
#pragma once
#endif

#include <clasp/constraint.h>
#include <clasp/util/atomic.h>
#include <clasp/util/misc_types.h>
#include <cassert>

namespace Clasp {
class MinimizeConstraint;
class WeightConstraint;


struct MinimizeMode_t {
        enum Mode {
                ignore    = 0, 
                optimize  = 1, 
                enumerate = 2, 
                enumOpt   = 3, 
        };
};
typedef MinimizeMode_t::Mode MinimizeMode;


class SharedMinimizeData {
public:
        typedef SharedMinimizeData ThisType;

        struct LevelWeight {
                LevelWeight(uint32 l, weight_t w) : level(l), next(0), weight(w) {}
                uint32   level : 31; 
                uint32   next  :  1; 
                weight_t weight;     
        };
        typedef PodVector<LevelWeight>::type WeightVec;
        explicit SharedMinimizeData(const SumVec& lhsAdjust, MinimizeMode m = MinimizeMode_t::optimize);
        ThisType*      share()               { ++count_; return this; }
        void           release()             { if (--count_ == 0) destroy(); }
        uint32         numRules()       const{ return static_cast<uint32>(adjust_.size()); }
        uint32         maxLevel()       const{ return numRules()-1; }
        static wsum_t  maxBound()            { return INT64_MAX; }
        MinimizeMode   mode()           const{ return mode_; }
        bool           optimize()       const{ return optGen_ ? checkNext() : mode_ != MinimizeMode_t::enumerate; }
        wsum_t         lower(uint32 x)  const{ return lower_[x]; }
        const wsum_t*  lower()          const{ return &lower_[0]; }
        wsum_t         upper(uint32 x)  const{ return upper()[x]; }
        const wsum_t*  upper()          const{ return &(opt_ + (gCount_ & 1u))->front(); }
        wsum_t         adjust(uint32 x) const{ return adjust_[x]; }
        wsum_t         optimum(uint32 x)const{ return adjust(x) + (mode_ != MinimizeMode_t::enumerate ? upper(x) : opt_[1][x]); }
        uint32         level(uint32 i)  const{ return numRules() == 1 ? 0 : weights[lits[i].second].level; }
        weight_t       weight(uint32 i) const{ return numRules() == 1 ? lits[i].second : weights[lits[i].second].weight; }
        uint32         generation()     const{ return gCount_; }
        bool           checkNext()      const{ return mode() != MinimizeMode_t::enumerate && generation() != optGen_; }
        bool heuristic(Solver& s, bool full) const;
        

        bool setMode(MinimizeMode m, const wsum_t* bound = 0, uint32 boundSize = 0);
        bool setMode(MinimizeMode m, const SumVec& bound) { return setMode(m, bound.empty() ? 0 : &bound[0], (uint32)bound.size()); }
        void resetBounds();
        

        MinimizeConstraint* attach(Solver& s, uint32 strat = UINT32_MAX, bool addRef = true);
        

        const SumVec* setOptimum(const wsum_t* opt);
        void          setLower(uint32 lev, wsum_t low);

        void          markOptimal();


        void add(wsum_t* lhs, const WeightLiteral& lit) const { if (weights.empty()) *lhs += lit.second; else add(lhs, &weights[lit.second]); }
        void add(wsum_t* lhs, const LevelWeight* w)     const { do { lhs[w->level] += w->weight; } while (w++->next); }
        void sub(wsum_t* lhs, const WeightLiteral& lit, uint32& aLev) const { if (weights.empty()) *lhs -= lit.second; else sub(lhs, &weights[lit.second], aLev); }
        void sub(wsum_t* lhs, const LevelWeight* w, uint32& aLev)     const;
        bool imp(wsum_t* lhs, const WeightLiteral& lit, const wsum_t* rhs, uint32& lev) const {
                return weights.empty() ? (*lhs+lit.second) > *rhs : imp(lhs, &weights[lit.second],  rhs, lev);
        }
        bool imp(wsum_t* lhs, const LevelWeight* w, const wsum_t* rhs, uint32& lev) const;
        weight_t weight(const WeightLiteral& lit, uint32 lev) const {
                if (numRules() == 1) { return lit.second * (lev == 0); }
                const LevelWeight* w = &weights[lit.second];
                do { if (w->level == lev) return w->weight; } while (w++->next);
                return 0;
        }
private:
        typedef Clasp::atomic<uint32> Atomic;
        SumVec       adjust_;  // initial bound adjustments
        SumVec       lower_;   // (unadjusted) lower bound of constraint
        SumVec       opt_[2];  // buffers for update via "double buffering"
        MinimizeMode mode_;    // how to compare assignments?
        Atomic       count_;   // number of refs to this object
        Atomic       gCount_;  // generation count - used when updating optimum
        uint32       optGen_;  // generation of optimal bound
public:
        WeightVec     weights; // sparse vectors of weights - only used for multi-level constraints
        WeightLiteral lits[0]; // (shared) literals - terminated with posLit(0)
private: 
        ~SharedMinimizeData();
        void destroy() const;
        SharedMinimizeData(const SharedMinimizeData&);
        SharedMinimizeData& operator=(const SharedMinimizeData&);
};

class MinimizeBuilder {
public:
        typedef SharedMinimizeData SharedData;
        MinimizeBuilder();
        ~MinimizeBuilder();
        
        bool             hasRules() const { return !adjust_.empty(); }
        uint32           numRules() const { return (uint32)adjust_.size(); }
        uint32           numLits()  const { return (uint32)lits_.size(); }

        MinimizeBuilder& addRule(const WeightLitVec& lits, wsum_t adjustSum = 0);
        MinimizeBuilder& addLit(uint32 lev, WeightLiteral lit);
        

        SharedData*      build(SharedContext& ctx);
        void clear();
private:
        struct Weight {
                Weight(uint32 lev, weight_t w) : level(lev), weight(w), next(0) {}
                uint32   level;
                weight_t weight;
                Weight*  next;
                static void free(Weight*& w);
        };
        typedef std::pair<Literal, Weight*> LitRep;
        typedef PodVector<LitRep>::type     LitRepVec;
        struct CmpByLit {
                bool operator()(const LitRep& lhs, const LitRep& rhs) const;
        };
        struct CmpByWeight {
                bool operator()(const LitRep& lhs, const LitRep& rhs) const;
                int  compare   (const LitRep& lhs, const LitRep& rhs) const;
        };
        void     unfreeze();
        bool     prepare(SharedContext& ctx);
        void     addTo(LitRep l, SumVec& vec);
        void     mergeReduceWeight(LitRep& x, LitRep& by);
        weight_t addFlattened(SharedData::WeightVec& x, const Weight& w);
        bool     eqWeight(const SharedData::LevelWeight* lhs, const Weight& rhs);
        weight_t addLitImpl(uint32 lev, WeightLiteral lit) {
                if (lit.second > 0) { lits_.push_back(LitRep(lit.first, new Weight(lev, lit.second)));   return 0; }
                if (lit.second < 0) { lits_.push_back(LitRep(~lit.first, new Weight(lev, -lit.second))); return lit.second; }
                return 0;
        }
        LitRepVec lits_;  // all literals
        SumVec    adjust_;// lhs adjustments
        bool      ready_; // prepare was called
};


class MinimizeConstraint : public Constraint {
public:
        typedef SharedMinimizeData       SharedData;
        typedef const SharedData*        SharedDataP;
        SharedDataP shared()  const { return shared_; } 
        virtual bool attach(Solver& s)    = 0;
        virtual bool integrate(Solver& s) = 0;

        virtual bool relax(Solver& s, bool reset) = 0;

        virtual bool handleModel(Solver& s) = 0;
        virtual bool handleUnsat(Solver& s, bool upShared, LitVec& restore) = 0;

        void         destroy(Solver*, bool);
        Constraint*  cloneAttach(Solver& other);
protected:
        MinimizeConstraint(SharedData* s);
        ~MinimizeConstraint();
        bool prepare(Solver& s, bool useTag);
        SharedData* shared_; // common shared data
        Literal     tag_;    // (optional) literal for tagging reasons
};


class DefaultMinimize : public MinimizeConstraint {
public:
        explicit DefaultMinimize(SharedData* d, uint32 strat);
        // base interface

        bool       attach(Solver& s);
        bool       integrate(Solver& s)           { return integrateBound(s); }
        bool       relax(Solver&, bool reset)     { return relaxBound(reset); }
        bool       handleModel(Solver& s)         { commitUpperBound(s); return true; }
        bool       handleUnsat(Solver& s, bool up, LitVec& out);
        // constraint interface
        PropResult propagate(Solver& s, Literal p, uint32& data);
        void       undoLevel(Solver& s);
        void       reason(Solver& s, Literal p, LitVec& lits);
        bool       minimize(Solver& s, Literal p, CCMinRecursive* r);
        void       destroy(Solver*, bool);
        // own interface
        bool       active()  const { return *opt() != SharedData::maxBound(); }
        uint32     numRules()const { return size_; }

        bool       integrateBound(Solver& s);


        void       commitUpperBound(const Solver& s);

        bool       commitLowerBound(const Solver& s, bool upShared);
        

        bool       relaxBound(bool full = false);

        bool       more() const { return step_.lev != size_; }

        // FOR TESTING ONLY!
        wsum_t sum(uint32 i, bool adjust) const { return sum()[i] + (adjust ? shared_->adjust(i):0); }
private:
        enum PropMode  { propagate_new_sum, propagate_new_opt };
        union UndoInfo;
        typedef const WeightLiteral* Iter;
        ~DefaultMinimize();
        // bound operations
        wsum_t* opt() const { return bounds_; }
        wsum_t* sum() const { return bounds_ + size_; }
        wsum_t* temp()const { return bounds_ + (size_*2); }
        wsum_t* end() const { return bounds_ + (size_*3); }
        void    assign(wsum_t* lhs, wsum_t* rhs)  const;
        bool    greater(wsum_t* lhs, wsum_t* rhs, uint32 len, uint32& aLev) const;
        // propagation & undo
        uint32  lastUndoLevel(const Solver& s) const;
        bool    litSeen(uint32 i) const;
        bool    propagateImpl(Solver& s, PropMode m);
        uint32  computeImplicationSet(const Solver& s, const WeightLiteral& it, uint32& undoPos);
        void    pushUndo(Solver& s, uint32 litIdx);
        bool    updateBounds(bool applyStep);
        // step
        wsum_t& stepLow() const { return *(end() + step_.lev); }
        void    stepInit(uint32 n);
        wsum_t*      bounds_;  // [upper,sum,temp[,lower]]
        Iter         pos_;     // position of literal to look at next
        UndoInfo*    undo_;    // one "seen" flag for each literal +
        uint32       undoTop_; // undo stack holding assigned literals
        uint32       posTop_;  // stack of saved "look at" positions
        const uint32 size_;    // number of rules
        uint32       actLev_;  // first level to look at when comparing bounds
        struct Step {          // how to reduce next tentative bound
        uint32 size;           //   size of step
        uint32 lev : 30;       //   level on which step is applied
        uint32 type:  2;       //   type of step (one of SolverStrategies::OptStrategy)
        }            step_;
};

class UncoreMinimize : public MinimizeConstraint {
public:
        // constraint interface
        PropResult propagate(Solver& s, Literal p, uint32& data);
        void       reason(Solver& s, Literal p, LitVec& lits);
        void       destroy(Solver*, bool);
        bool       simplify(Solver& s, bool reinit = false);
        // base interface
        bool       attach(Solver& s);
        bool       integrate(Solver& s);
        bool       relax(Solver&, bool reset);
        bool       valid(Solver& s);
        bool       handleModel(Solver& s);
        bool       handleUnsat(Solver& s, bool up, LitVec& out);
private:
        friend class SharedMinimizeData;
        explicit UncoreMinimize(SharedData* d, bool preprocess);
        typedef DefaultMinimize* EnumPtr;
        struct LitData {
                LitData(weight_t w, bool as, uint32 c) : weight(w), coreId(c), assume((uint32)as) {}
                weight_t weight;
                uint32   coreId : 31;
                uint32   assume :  1;
        };
        struct LitPair {
                LitPair(Literal p, uint32 dataId) : lit(p), id(dataId) {}
                Literal lit;
                uint32  id;
        };
        struct Core {
                Core(WeightConstraint* c, weight_t b, weight_t w) : con(c), bound(b), weight(w) {}
                uint32  size()       const;
                Literal at(uint32 i) const;
                Literal tag()        const;
                WeightConstraint* con;
                weight_t          bound;
                weight_t          weight;
        };
        struct WCTemp {
                typedef WeightLitVec WLitVec;
                void     start(weight_t b){ lits.clear(); bound = b; }
                void     add(Solver& s, Literal p);
                bool     unsat() const { return bound > 0 && static_cast<uint32>(bound) > static_cast<uint32>(lits.size()); }
                weight_t bound;
                WLitVec  lits;
        };
        typedef PodVector<LitData>::type     LitTable;
        typedef PodVector<Core>::type        CoreTable;
        typedef PodVector<Constraint*>::type ConTable;
        typedef PodVector<LitPair>::type     LitSet;
        // literal and core management
        bool     hasCore(const LitData& x) const { return x.coreId != 0; }
        LitData& getData(uint32 id)              { return litData_[id-1];}
        Core&    getCore(const LitData& x)       { return open_[x.coreId-1]; }
        LitData& addLit(Literal p, weight_t w);
        void     releaseLits();
        bool     addCore(Solver& s, const LitPair* lits, uint32 size, weight_t weight);
        bool     addCore(Solver& s, const WCTemp& wc, weight_t w);
        bool     closeCore(Solver& s, LitData& x, bool sat);
        uint32   allocCore(WeightConstraint* con, weight_t bound, weight_t weight, bool open);
        // algorithm
        void     init();
        uint32   initRoot(Solver& s);
        bool     initLevel(Solver& s);
        uint32   analyze(Solver& s, LitVec& cfl, weight_t& minW, LitVec& poppedOther);
        bool     pushPath(Solver& s);
        void     integrateOpt(Solver& s);
        bool     popPath(Solver& s, uint32 dl, LitVec& out);
        bool     fixLit(Solver& s, Literal p);
        bool     fixLevel(Solver& s);
        void     detach(Solver* s, bool b);
        wsum_t*  computeSum(Solver& s) const;
        void     setLower(wsum_t x) {
                if (!pre_ && x > lower_) { lower_ = x; }
        }
        bool    validLowerBound() const {
                wsum_t cmp = lower_ - upper_;
                return cmp < 0 || (cmp == 0 && level_ == shared_->maxLevel() && !shared_->checkNext());
        }
        // data
        EnumPtr   enum_;      // for supporting (optimal) model enumeration in parallel mode
        wsum_t*   sum_;       // costs of active model
        LitTable  litData_;   // data for active literals (tag lits for cores + lits from active minimize)
        CoreTable open_;      // open cores, i.e. relaxable and referenced by an assumption
        ConTable  closed_;    // closed cores represented as weight constraints
        LitSet    assume_;    // current set of assumptions
        LitSet    todo_;      // core(s) not yet represented as constraint
        LitVec    fix_;       // set of fixed literals
        LitVec    conflict_;  // current conflict
        WCTemp    temp_;      // temporary: used for creating weight constraints
        wsum_t    lower_;     // lower bound of active level
        wsum_t    upper_;     // upper bound of active level
        uint32    auxInit_;   // number of solver aux vars on attach
        uint32    auxAdd_;    // number of aux vars added for cores
        uint32    gen_;       // active generation
        uint32    level_ : 25;// active level
        uint32    valid_ :  1;// valid w.r.t active generation?
        uint32    hasPre_:  1;// use preprocessing?
        uint32    sat_   :  1;// update because of model
        uint32    pre_   :  1;// preprocessing active?
        uint32    path_  :  1;// push path?
        uint32    next_  :  1;// assume next level?
        uint32    init_  :  1;// init constraint?
        uint32    eRoot_;     // saved root level of solver (initial gp)
        uint32    aTop_;      // saved assumption level (added by us)
        uint32    freeOpen_;  // head of open core free list
};

} // end namespace Clasp

#endif