Clasp::SatPreParams Struct Reference

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

#include <solver_strategies.h>

List of all members.

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
uint32	bce () const
bool	clauseLimit (uint32 nc) const
void	disableBce ()
bool	occLimit (uint32 pos, uint32 neg) const
	SatPreParams ()
Static Public Member Functions
static SatPreprocessor *	create (const SatPreParams &)
Public Attributes
uint32	limClause: 16
uint32	limFrozen: 7
uint32	limIters: 10
uint32	limOcc: 16
uint32	limTime: 12
uint32	mode: 1
uint32	type: 2

---

Detailed Description

Parameters for (optional) Sat-preprocessing.

Definition at line 333 of file solver_strategies.h.

---

Member Enumeration Documentation

enum Clasp::SatPreParams::Mode

Enumerator:

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

Definition at line 334 of file solver_strategies.h.

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.

Definition at line 338 of file solver_strategies.h.

---

Constructor & Destructor Documentation

Clasp::SatPreParams::SatPreParams

(

)

[inline]

Definition at line 344 of file solver_strategies.h.

---

Member Function Documentation

uint32 Clasp::SatPreParams::bce

(

)

const [inline]

Definition at line 354 of file solver_strategies.h.

bool Clasp::SatPreParams::clauseLimit

(

uint32

nc

)

const [inline]

Definition at line 352 of file solver_strategies.h.

SatPreprocessor * Clasp::SatPreParams::create

(

const SatPreParams &

opts

)

[static]

Definition at line 615 of file satelite.cpp.

void Clasp::SatPreParams::disableBce

(

)

[inline]

Definition at line 355 of file solver_strategies.h.

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

Definition at line 353 of file solver_strategies.h.

---

Member Data Documentation

uint32 Clasp::SatPreParams::limClause

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

Definition at line 350 of file solver_strategies.h.

uint32 Clasp::SatPreParams::limFrozen

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

Definition at line 349 of file solver_strategies.h.

uint32 Clasp::SatPreParams::limIters

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

Definition at line 347 of file solver_strategies.h.

uint32 Clasp::SatPreParams::limOcc

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

Definition at line 351 of file solver_strategies.h.

uint32 Clasp::SatPreParams::limTime

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

Definition at line 348 of file solver_strategies.h.

uint32 Clasp::SatPreParams::mode

One of mode.

Definition at line 346 of file solver_strategies.h.

uint32 Clasp::SatPreParams::type

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

Definition at line 345 of file solver_strategies.h.

---

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

• solver_strategies.h
• satelite.cpp