Inheritance diagram for Clasp::SolverStrategies:

Public Types
enum	CCMinAntes { no_antes = 0, all_antes = 1, short_antes = 2, binary_antes = 3 }
	Antecedents to consider during conflict clause minimization. More...
enum	CCRepMode { cc_no_replace = 0, cc_rep_decision = 1, cc_rep_uip = 2, cc_rep_dynamic = 3 }
	Simplifications for long conflict clauses. More...
enum	OptHeu { opt_sign = 1, opt_model = 2 }
enum	OptStrategy { opt_def = 0, opt_hier = 1, opt_inc = 2, opt_dec = 3, opt_unsat = 4, opt_unsat_pre = 5 }
	Strategy to use when optimization is active. More...
enum	SearchStrategy { use_learning = 0, no_learning = 1 }
	Clasp's two general search strategies. More...
enum	SignHeu { sign_atom = 0, sign_no = 1, sign_yes = 2, sign_rnd = 3, sign_disj = 4 }
	Default sign heuristic. More...
enum	UpdateMode { update_on_propagate = 0, update_on_conflict = 1 }
enum	WatchInit { watch_first = 0, watch_rand = 1, watch_least = 2 }
Public Member Functions
void	prepare ()
	SolverStrategies ()
Public Attributes
uint32	bumpVarAct: 1
uint32	ccMinAntes: 2
uint32	ccRepMode: 2
uint32	compress: 16
uint32	heuReserved: 3
uint32	id: 6
uint32	initWatches: 2
uint32	loadCfg: 1
uint32	optHeu: 2
uint32	otfs: 2
uint32	restartOnModel: 1
uint32	reverseArcs: 2
uint32	saveProgress: 16
uint32	search: 1
uint32	signDef: 3
uint32	signFix: 1
uint32	updateLbd: 2
uint32	upMode: 1

Detailed Description

Definition at line 97 of file solver_strategies.h.

Member Enumeration Documentation

Antecedents to consider during conflict clause minimization.

Enumerator:

no_antes	Don't minimize first-uip-clauses.
all_antes	Consider all antecedents.
short_antes	Consider only short antecedents.
binary_antes	Consider only binary antecedents.

Definition at line 112 of file solver_strategies.h.

Simplifications for long conflict clauses.

Enumerator:

cc_no_replace	Don't replace literals in conflict clauses.
cc_rep_decision	Replace conflict clause with decision sequence.
cc_rep_uip	Replace conflict clause with all uip clause.
cc_rep_dynamic	Dynamically select between cc_rep_decision and cc_rep_uip.

Definition at line 119 of file solver_strategies.h.

Enumerator:

opt_sign	Use optimize statements in sign heuristic.
opt_model	Apply model heuristic when optimizing.

Definition at line 125 of file solver_strategies.h.

Strategy to use when optimization is active.

Enumerator:

opt_def	Use default branch and bound optimization.
opt_hier	Use hierarchical branch and bound optimization.
opt_inc	Use hierarchical optimization with increasing steps.
opt_dec	Use hierarchical optimization with decreasing steps.
opt_unsat	Use unsat-core based optimization.
opt_unsat_pre	Use unsat-core based optimization with preprocessing.

Definition at line 130 of file solver_strategies.h.

Clasp's two general search strategies.

Enumerator:

use_learning	Analyze conflicts and learn First-1-UIP-clause
no_learning	Don't analyze conflicts - chronological backtracking

Definition at line 99 of file solver_strategies.h.

Default sign heuristic.

Enumerator:

sign_atom	Prefer negative literal for atoms.
sign_no	Always prefer positive literal.
sign_yes	Always prefer negative literal.
sign_rnd	Prefer random literal.
sign_disj	Prefer negative literal for atoms in hcf-components.