SatMinisat_ptr 
SatMinisat_create(
  const char* name 
)
The first parameter is the name of the solver.

Defined in SatMinisat.c 

void 
SatMinisat_destroy(
  SatMinisat_ptr  self 
)
Destroys an instance of a MiniSat SAT solver

Defined in SatMinisat.c 

SatZchaff_ptr 
SatZchaff_create(
  const char* name 
)
The first parameter is the name of the solver.

Defined in SatZchaff.c 

void 
SatZchaff_destroy(
  SatZchaff_ptr  self 
)
The first parameter is the name of the solver.

Defined in SatZchaff.c 

static int 
_get_clause_size(
  const int * clause 
)
Computes the size of a clause.

Defined in SatMinisat.c 

static int 
_get_clause_size(
  const int * clause 
)
Computes the size of a clause.

Defined in SatZchaff.c 

void 
sat_minisat_add(
  const SatSolver_ptr  solver, 
  const Be_Cnf_ptr  cnfProb, 
  SatSolverGroup  group 
)
converts all CNF literals into the internal literals, adds a group id to every clause (if group is not permament) and then add obtained clauses to actual Minisat

Defined in SatMinisat.c 

void 
sat_minisat_clear_preferred_variables(
  const SatSolver_ptr  solver 
)
Clears preferred variables in the solver. A preferred variable is split upon with priority, with respect to non-preferedd ones.

See Also SatSolver_set_preferred_variables
Defined in SatMinisat.c 

int 
sat_minisat_cnfLiteral2minisatLiteral(
  SatMinisat_ptr  self, 
  int  cnfLiteral 
)
The literal may not be 0 (because 0 cannot have sign). First, the function obtains the cnf variable (removes the sign), obtains associated internal var through hash table(creates if necessary an internal variable) and then converts it in minisat literal (just adjust the sign). If necessary a new minisat variable is created.

See Also sat_minisat_minisatLiteral2cnfLiteral
Defined in SatMinisat.c 

SatSolverGroup 
sat_minisat_create_group(
  const SatIncSolver_ptr  solver 
)
Adds the group at the END of the existing groups list

See Also SatIncSolver_destroy_group SatIncSolver_move_to_permanent_and_destroy_group
Defined in SatMinisat.c 

void 
sat_minisat_deinit(
  SatMinisat_ptr  self 
)
Deinitializes SatMinisat object.

Defined in SatMinisat.c 

void 
sat_minisat_destroy_group(
  const SatIncSolver_ptr  solver, 
  SatSolverGroup  group 
)
Just adds to the solver a unit clause with positive literal of a variable with index equal to group id

See Also SatIncSolver_create_group
Defined in SatMinisat.c 

void 
sat_minisat_enlarge_minisatClause(
  const SatMinisat_ptr  self, 
  unsigned int  minSize 
)
Enlarges minisatClause until it has at least size minSize.

Side Effects minisatClause might be reallocated, minisatClauseSize changes value.

See Also sat_minisat_add
Defined in SatMinisat.c 

static void 
sat_minisat_finalize(
  Object_ptr  object, 
  void* dummy 
)
Pure virtual function. This must be refined by derived classes.

Defined in SatMinisat.c 

Slist_ptr 
sat_minisat_get_conflicts(
  const SatSolver_ptr  solver 
)
Only use with SatMinisat_solve_permanent_group_assume

See Also sat_minisat_solve_permanent_group_assume sat_minisat_make_conflicts
Defined in SatMinisat.c 

int 
sat_minisat_get_minisatClauseSize(
  const SatMinisat_ptr  self 
)
Getter for minisatClauseSize

Defined in SatMinisat.c 

int* 
sat_minisat_get_minisatClause(
  const SatMinisat_ptr  self 
)
Getter for minisatClause

Defined in SatMinisat.c 

int 
sat_minisat_get_polarity_mode(
  const SatSolver_ptr  solver 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function. It is an error if the last solving was unsuccessful.

Defined in SatMinisat.c 

void 
sat_minisat_init(
  SatMinisat_ptr  self, 
  const char* name 
)
Initializes Sat Minisat object.

Defined in SatMinisat.c 

Slist_ptr 
sat_minisat_make_conflicts(
  const SatMinisat_ptr  self 
)
Obtains the set of conflicting assumptions from MiniSat

See Also sat_minisat_solve_permanent_group_assume sat_minisat_get_conflict
Defined in SatMinisat.c 

Slist_ptr 
sat_minisat_make_model(
  const SatSolver_ptr  solver 
)
The previous invocation of SAT_Solve should have been successful

Defined in SatMinisat.c 

int 
sat_minisat_minisatLiteral2cnfLiteral(
  SatMinisat_ptr  self, 
  int  minisatLiteral 
)
The variable in the literal has to be created by sat_minisat_cnfLiteral2minisatLiteral only. First, the function obtains the minisat variable from the literal, obtains associated cnf variable (there must already be the association), and then converts it in cnf literal (adjust the sign)

See Also sat_minisat_cnfLiteral2minisatLiteral
Defined in SatMinisat.c 

void 
sat_minisat_move_to_permanent_and_destroy_group(
  const SatIncSolver_ptr  solver, 
  SatSolverGroup  group 
)
just adds to minisat a unit clause with negative literal of a variable with index equal to group id

See Also SatIncSolver_create_group SatSolver_get_permanent_group
Defined in SatMinisat.c 

void 
sat_minisat_set_polarity_mode(
  SatSolver_ptr  solver, 
  int  mode 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function. It is an error if the last solving was unsuccessful.

Defined in SatMinisat.c 

void 
sat_minisat_set_polarity(
  const SatSolver_ptr  solver, 
  const Be_Cnf_ptr  cnfProb, 
  int  polarity, 
  SatSolverGroup  group 
)
Sets the polarity of the formula. Polarity 1 means the formula is considered as positive, and -1 means the negation of the formula will be solved. A unit clause of the literal (with sign equal to polarity) corresponding to the given CNF formula is added to the solve.

Defined in SatMinisat.c 

void 
sat_minisat_set_preferred_variables(
  const SatSolver_ptr  solver, 
  const Slist_ptr  cnfVars 
)
Sets preferred variables in the solver. A preferred variable is split upon with priority, with respect to non-preferedd ones.

See Also SatSolver_clear_preferred_variables
Defined in SatMinisat.c 

void 
sat_minisat_set_random_mode(
  SatSolver_ptr  solver, 
  double  seed 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function. It is an error if the last solving was unsuccessful.

Defined in SatMinisat.c 

SatSolverResult 
sat_minisat_solve_all_groups(
  const SatSolver_ptr  solver 
)
Tries to solve all added formulas

Defined in SatMinisat.c 

SatSolverResult 
sat_minisat_solve_groups(
  const SatIncSolver_ptr  solver, 
  const Olist_ptr  groups 
)
The permanent group is automatically added to the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

Defined in SatMinisat.c 

SatSolverResult 
sat_minisat_solve_permanent_group_assume(
  const SatSolver_ptr  sol, 
  const Slist_ptr  assumptions 
)
Obtain set of conflicting assumptions with sat_minisat_get_conflict

See Also sat_minisat_get_conflict sat_minisat_make_conflicts
Defined in SatMinisat.c 

SatSolverResult 
sat_minisat_solve_without_groups(
  const SatIncSolver_ptr  solver, 
  const Olist_ptr  groups 
)
The permanent group must not be in the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

See Also SatSolverResult SatSolver_get_permanent_group SatIncSolver_create_group SatSolver_get_model
Defined in SatMinisat.c 

void 
sat_zchaff_add(
  const SatSolver_ptr  solver, 
  const Be_Cnf_ptr  cnfProb, 
  SatSolverGroup  group 
)
converts all CNF literals into the internal literals, adds a group id to every clause (if group is not permament) and then add obtained clauses to actual ZChaff

Defined in SatZchaff.c 

void 
sat_zchaff_clear_preferred_variables(
  const SatSolver_ptr  solver 
)
Clears preferred variables in the solver

See Also sat_zchaff_set_preferred_variables
Defined in SatZchaff.c 

int 
sat_zchaff_cnfLiteral2zchaffLiteral(
  SatZchaff_ptr  self, 
  int  cnfLiteral 
)
The literal may not be 0 (because 0 cannot have sign). First, the function obtains the cnf variable (removes the sign), obtains associated internal var through hash table(creates if necessary an internal variable) and then converts it in zchaff literal (var*2+sign, see ZChaff SAT.h). If necessary a new minisat variable is created.

See Also sat_zchaff_zchaffLiteral2cnfLiteral
Defined in SatZchaff.c 

SatSolverGroup 
sat_zchaff_create_group(
  const SatIncSolver_ptr  solver 
)
Adds the group at the END of the existing groups list

See Also SatIncSolver_destroy_group SatIncSolver_move_to_permanent_and_destroy_group
Defined in SatZchaff.c 

void 
sat_zchaff_deinit(
  SatZchaff_ptr  self 
)
Deinitializes SatZchaff object.

Defined in SatZchaff.c 

void 
sat_zchaff_destroy_group(
  const SatIncSolver_ptr  solver, 
  SatSolverGroup  group 
)
Just adds to the solver a unit clause with positive literal of a variable with index equal to group id

See Also SatIncSolver_create_group
Defined in SatZchaff.c 

static void 
sat_zchaff_finalize(
  Object_ptr  object, 
  void* dummy 
)
Pure virtual function. This must be refined by derived classes.

Defined in SatZchaff.c 

Slist_ptr 
sat_zchaff_get_conflicts(
  const SatSolver_ptr  self 
)
Only use with SatMinisat_solve_permanent_group_assume

See Also sat_minisat_solve_permanent_group_assume sat_minisat_make_conflict
Defined in SatZchaff.c 

void 
sat_zchaff_init(
  SatZchaff_ptr  self, 
  const char* name 
)
Initializes Sat Zchaff object.

Defined in SatZchaff.c 

Slist_ptr 
sat_zchaff_make_conflicts(
  const SatZchaff_ptr  self 
)
Obtains the set of conflicting assumptions from zCahdd

See Also sat_zchaff_solve_permanent_group_assume sat_zchaff_get_conflict
Defined in SatZchaff.c 

Slist_ptr 
sat_zchaff_make_model(
  const SatSolver_ptr  solver 
)
The previous invocation of SAT_Solve should have been successful

Defined in SatZchaff.c 

void 
sat_zchaff_move_to_permanent_and_destroy_group(
  const SatIncSolver_ptr  solver, 
  SatSolverGroup  group 
)
just adds to zchaff a unit clause with negative literal of a variable with index equal to group id

See Also SatIncSolver_create_group SatSolver_get_permanent_group
Defined in SatZchaff.c 

void 
sat_zchaff_set_polarity(
  const SatSolver_ptr  solver, 
  const Be_Cnf_ptr  cnfProb, 
  int  polarity, 
  SatSolverGroup  group 
)
Sets the polarity of the formula. Polarity 1 means the formula is considered as positive, and -1 means the negation of the formula will be solved. A unit clause of the literal (with sign equal to polarity) corresponding to the given CNF formula is added to the solve.

Defined in SatZchaff.c 

void 
sat_zchaff_set_preferred_variables(
  const SatSolver_ptr  solver, 
  const Slist_ptr  cnfVars 
)
Sets preferred variables in the solver

See Also sat_zchaff_clear_preferred_variables
Defined in SatZchaff.c 

SatSolverResult 
sat_zchaff_solve_all_groups(
  const SatSolver_ptr  solver 
)
Tries to solve all added formulas

Defined in SatZchaff.c 

SatSolverResult 
sat_zchaff_solve_groups(
  const SatIncSolver_ptr  solver, 
  const Olist_ptr  groups 
)
The permanent group is automatically added to the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

Defined in SatZchaff.c 

SatSolverResult 
sat_zchaff_solve_permanent_group_assume(
  const SatSolver_ptr  self, 
  const Slist_ptr  assumptions 
)
Obtain set of conflicting assumptions with sat_minisat_get_conflict

See Also sat_zchaff_get_conflict sat_zchaff_make_conflict
Defined in SatZchaff.c 

SatSolverResult 
sat_zchaff_solve_without_groups(
  const SatIncSolver_ptr  solver, 
  const Olist_ptr  groups 
)
The permanent group must not be in the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

See Also SatSolverResult SatSolver_get_permanent_group SatIncSolver_create_group SatSolver_get_model
Defined in SatZchaff.c 

int 
sat_zchaff_zchaffLiteral2cnfLiteral(
  SatZchaff_ptr  self, 
  int  zchaffLiteral 
)
The variable in the literal has to be created by sat_zchaff_cnfLiteral2zchaffLiteral only. First, the function obtains the zchaff variable from the literal, obtains associated cnf variable (there must already be the association), and then converts it in cnf literal (add the sign)

See Also sat_zchaff_cnfLiteral2zchaffLiteral
Defined in SatZchaff.c
Last updated on 2011/04/06 21h:12