Clasp::SatPreParams Struct Reference

Parameters for (optional) Sat-preprocessing. More...

#include <solver_strategies.h>

Collaboration diagram for Clasp::SatPreParams:

Public Types
enum	Mode { prepro_preserve_sat = 0, prepro_preserve_models = 1 }
enum	Type { sat_pre_no = 0, sat_pre_ve = 1, sat_pre_ve_bce = 2, sat_pre_full = 3 }

Public Member Functions
	SatPreParams ()
bool	clauseLimit (uint32 nc) const
bool	occLimit (uint32 pos, uint32 neg) const
uint32	bce () const
void	disableBce ()

Static Public Member Functions
static SatPreprocessor *	create (const SatPreParams &)

Public Attributes
uint32	type: 2
uint32	mode: 1
uint32	limIters: 10
uint32	limTime: 12
uint32	limFrozen: 7
uint32	limClause: 16
uint32	limOcc: 16

Detailed Description

Parameters for (optional) Sat-preprocessing.

Member Enumeration Documentation

enum Clasp::SatPreParams::Mode

Enumerator
prepro_preserve_sat	Allow full preprocessing.
prepro_preserve_models	Only allow model-preserving preprocessing.

enum Clasp::SatPreParams::Type

Enumerator
sat_pre_no	Disable sat-preprocessing.
sat_pre_ve	Run variable elimination.
sat_pre_ve_bce	Run variable- and limited blocked clause elimination.
sat_pre_full	Run variable- and full blocked clause elimination.

Constructor & Destructor Documentation

Clasp::SatPreParams::SatPreParams ( )

inline

Member Function Documentation

uint32 Clasp::SatPreParams::bce ( ) const

inline

bool Clasp::SatPreParams::clauseLimit ( uint32  nc ) const

inline

SatPreprocessor * Clasp::SatPreParams::create ( const SatPreParams &  opts )

static

void Clasp::SatPreParams::disableBce ( )

inline

bool Clasp::SatPreParams::occLimit ( uint32  pos, uint32  neg  ) const

inline

Member Data Documentation

uint32 Clasp::SatPreParams::limClause

Run only if #clauses < (limClause*1000) (0=no limit)

uint32 Clasp::SatPreParams::limFrozen

Run only if percent of frozen vars < maxFrozen. (0=no limit)

uint32 Clasp::SatPreParams::limIters

Max. number of iterations. (0=no limit)

uint32 Clasp::SatPreParams::limOcc

Skip v, if #occ(v) >= limOcc && #occ(~v) >= limOcc.(0=no limit)

uint32 Clasp::SatPreParams::limTime

Max. runtime in sec, checked after each iteration. (0=no limit)

uint32 Clasp::SatPreParams::mode

One of mode.

uint32 Clasp::SatPreParams::type

Blocked clause elimination (0=off, 1=limited, 2=full).

---

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

• /Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/solver_strategies.h
• /Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/satelite.cpp