Classes | Public Member Functions | Protected Member Functions | Private Types | Private Member Functions | Private Attributes
Clasp::SatElite::SatElite Class Reference

SatElite preprocessor for clauses. More...

#include <satelite.h>

Inheritance diagram for Clasp::SatElite::SatElite:
Inheritance graph
[legend]

List of all members.

Classes

struct  LessOccCost
struct  OccurList
struct  Progress

Public Member Functions

Clasp::SatPreprocessor * clone ()
 Creates a clone of this preprocessor.
 SatElite ()
 ~SatElite ()

Protected Member Functions

void doCleanUp ()
void doExtendModel (ValueVec &m, LitVec &open)
bool doPreprocess ()
bool initPreprocess (Options &opts)
void reportProgress (Progress::EventOp, uint32 curr, uint32 max)

Private Types

typedef ClWList::left_iterator ClIter
typedef std::pair< ClIter, ClIter > ClRange
typedef
bk_lib::left_right_sequence
< Literal, Var, 0 > 		ClWList
typedef
bk_lib::indexed_priority_queue
< LessOccCost > 		ElimHeap
typedef PodVector< uint8 >::type TouchedList
typedef ClWList::right_iterator WIter

Private Member Functions

bool addResolvent (uint32 newId, const Clause &c1, const Clause &c2)
void addToSubQueue (uint32 clauseId)
void attach (uint32 cId, bool initialClause)
bool backwardSubsume ()
bool bce ()
bool bceVe (Var v, uint32 maxCnt)
void bceVeRemove (uint32 cId, bool freeId, Var v, bool blocked)
bool cutoff (Var v) const
void detach (uint32 cId)
bool eliminateVars ()
uint32 findUnmarkedLit (const Clause &c, uint32 x) const
void markAll (const Literal *lits, uint32 size) const
const SatElite & operator= (const SatElite &)
Clause * peekSubQueue () const
Clause * popSubQueue ()
bool propagateFacts ()
 SatElite (const SatElite &)
ClRange splitOcc (Var v, bool mark)
bool strengthenClause (uint32 clauseId, Literal p)
bool subsumed (LitVec &cl)
Literal subsumes (const Clause &c, const Clause &other, Literal res) const
bool timeout () const
bool trivialResolvent (const Clause &c2, Var v) const
void unmarkAll (const Literal *lits, uint32 size) const
void updateHeap (Var v)

Private Attributes

ElimHeap elimHeap_
uint32 facts_
VarVec negT_
OccurList * occurs_
const Options * opts_
VarVec posT_
uint32 qFront_
VarVec queue_
ClauseList resCands_
LitVec resolvent_
std::time_t timeout_

Detailed Description

SatElite preprocessor for clauses.

The preprocessor implements subsumption, self-subsumption, variable elimination, and (optionally) blocked clause elimination.

See also:
  • Niklas Eén, Armin Biere: "Effective Preprocessing in SAT through Variable and Clause Elimination"
  • Matti Järvisalo, Armin Biere, Marijn Heule: "Blocked Clause Elimination"
  • Parts of the SatElite preprocessor are adapted from MiniSAT 2.0 beta available under the MIT licence from http://minisat.se/MiniSat.html

Definition at line 44 of file satelite.h.

Member Typedef Documentation

typedef ClWList::left_iterator Clasp::SatElite::SatElite::ClIter [private]

Definition at line 67 of file satelite.h.

typedef std::pair<ClIter, ClIter> Clasp::SatElite::SatElite::ClRange [private]

Definition at line 69 of file satelite.h.

typedef bk_lib::left_right_sequence<Literal, Var,0> Clasp::SatElite::SatElite::ClWList [private]

Definition at line 66 of file satelite.h.

typedef bk_lib::indexed_priority_queue<LessOccCost> Clasp::SatElite::SatElite::ElimHeap [private]

Definition at line 116 of file satelite.h.

typedef PodVector<uint8>::type Clasp::SatElite::SatElite::TouchedList [private]

Definition at line 65 of file satelite.h.

typedef ClWList::right_iterator Clasp::SatElite::SatElite::WIter [private]

Definition at line 68 of file satelite.h.

Constructor & Destructor Documentation

Clasp::SatElite::SatElite::SatElite ( )

Definition at line 31 of file satelite.cpp.

Clasp::SatElite::SatElite::~SatElite ( )

Definition at line 38 of file satelite.cpp.

Clasp::SatElite::SatElite::SatElite ( const SatElite &  ) [private]

Member Function Documentation

bool Clasp::SatElite::SatElite::addResolvent ( uint32  newId,
const Clause &  c1,
const Clause &  c2 
) [private]

Definition at line 512 of file satelite.cpp.

void Clasp::SatElite::SatElite::addToSubQueue ( uint32  clauseId) [inline, private]

Definition at line 70 of file satelite.cpp.

void Clasp::SatElite::SatElite::attach ( uint32  cId,
bool  initialClause 
) [private]

Definition at line 78 of file satelite.cpp.

bool Clasp::SatElite::SatElite::backwardSubsume ( ) [private]

Definition at line 177 of file satelite.cpp.

bool Clasp::SatElite::SatElite::bce ( ) [private]

Definition at line 466 of file satelite.cpp.

bool Clasp::SatElite::SatElite::bceVe ( Var  v,
uint32  maxCnt 
) [private]

Definition at line 389 of file satelite.cpp.

void Clasp::SatElite::SatElite::bceVeRemove ( uint32  cId,
bool  freeId,
Var  v,
bool  blocked 
) [private]

Definition at line 109 of file satelite.cpp.

Clasp::SatPreprocessor * Clasp::SatElite::SatElite::clone ( ) [virtual]

Creates a clone of this preprocessor.

Note:
The function does not clone any clauses already added to *this.

Implements Clasp::SatPreprocessor.

Definition at line 46 of file satelite.cpp.

bool Clasp::SatElite::SatElite::cutoff ( Var  v) const [inline, private]

Definition at line 150 of file satelite.h.

void Clasp::SatElite::SatElite::detach ( uint32  cId) [private]

Definition at line 98 of file satelite.cpp.

void Clasp::SatElite::SatElite::doCleanUp ( ) [protected, virtual]

Implements Clasp::SatPreprocessor.

Definition at line 51 of file satelite.cpp.

void Clasp::SatElite::SatElite::doExtendModel ( ValueVec &  m,
LitVec &  open 
) [protected, virtual]

Implements Clasp::SatPreprocessor.

Definition at line 552 of file satelite.cpp.

bool Clasp::SatElite::SatElite::doPreprocess ( ) [protected, virtual]

Implements Clasp::SatPreprocessor.

Definition at line 137 of file satelite.cpp.

bool Clasp::SatElite::SatElite::eliminateVars ( ) [private]

Definition at line 481 of file satelite.cpp.

uint32 Clasp::SatElite::SatElite::findUnmarkedLit ( const Clause &  c,
uint32  x 
) const [inline, private]

Definition at line 268 of file satelite.cpp.

bool Clasp::SatElite::SatElite::initPreprocess ( Options &  opts) [protected, virtual]

Implements Clasp::SatPreprocessor.

Definition at line 129 of file satelite.cpp.

void Clasp::SatElite::SatElite::markAll ( const Literal *  lits,
uint32  size 
) const [private]

Definition at line 374 of file satelite.cpp.

const SatElite& Clasp::SatElite::SatElite::operator= ( const SatElite &  ) [private]
Clause* Clasp::SatElite::SatElite::peekSubQueue ( ) const [inline, private]

Definition at line 117 of file satelite.h.

SatPreprocessor::Clause * Clasp::SatElite::SatElite::popSubQueue ( ) [inline, private]

Definition at line 62 of file satelite.cpp.

bool Clasp::SatElite::SatElite::propagateFacts ( ) [private]

Definition at line 157 of file satelite.cpp.

void Clasp::SatElite::SatElite::reportProgress ( Progress::EventOp  id,
uint32  curr,
uint32  max 
) [protected]

Definition at line 42 of file satelite.cpp.

SatElite::ClRange Clasp::SatElite::SatElite::splitOcc ( Var  v,
bool  mark 
) [private]

Definition at line 356 of file satelite.cpp.

bool Clasp::SatElite::SatElite::strengthenClause ( uint32  clauseId,
Literal  p 
) [private]

Definition at line 335 of file satelite.cpp.

bool Clasp::SatElite::SatElite::subsumed ( LitVec &  cl) [private]

Definition at line 281 of file satelite.cpp.

Literal Clasp::SatElite::SatElite::subsumes ( const Clause &  c,
const Clause &  other,
Literal  res 
) const [private]

Definition at line 236 of file satelite.cpp.

bool Clasp::SatElite::SatElite::timeout ( ) const [inline, private]

Definition at line 154 of file satelite.h.

bool Clasp::SatElite::SatElite::trivialResolvent ( const Clause &  c2,
Var  v 
) const [private]

Definition at line 500 of file satelite.cpp.

void Clasp::SatElite::SatElite::unmarkAll ( const Literal *  lits,
uint32  size 
) const [private]

Definition at line 379 of file satelite.cpp.

void Clasp::SatElite::SatElite::updateHeap ( Var  v) [inline, private]

Definition at line 123 of file satelite.h.

Member Data Documentation

ElimHeap Clasp::SatElite::SatElite::elimHeap_ [private]

Definition at line 157 of file satelite.h.

uint32 Clasp::SatElite::SatElite::facts_ [private]

Definition at line 163 of file satelite.h.

VarVec Clasp::SatElite::SatElite::negT_ [private]

Definition at line 158 of file satelite.h.

OccurList* Clasp::SatElite::SatElite::occurs_ [private]

Definition at line 156 of file satelite.h.

const Options* Clasp::SatElite::SatElite::opts_ [private]

Definition at line 155 of file satelite.h.

VarVec Clasp::SatElite::SatElite::posT_ [private]

Definition at line 158 of file satelite.h.

uint32 Clasp::SatElite::SatElite::qFront_ [private]

Definition at line 162 of file satelite.h.

VarVec Clasp::SatElite::SatElite::queue_ [private]

Definition at line 161 of file satelite.h.

ClauseList Clasp::SatElite::SatElite::resCands_ [private]

Definition at line 159 of file satelite.h.

LitVec Clasp::SatElite::SatElite::resolvent_ [private]

Definition at line 160 of file satelite.h.

std::time_t Clasp::SatElite::SatElite::timeout_ [private]

Definition at line 164 of file satelite.h.

The documentation for this class was generated from the following files:

clasp
Author(s): Benjamin Kaufmann
autogenerated on Thu Aug 27 2015 12:41:41