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

SatSim_ptr 
SatSim_create(
  const char* name 
)
The first parameter is the name of the solver.

Defined in SatSim.c

void 
SatSim_destroy(
  SatSim_ptr  self 
)
Destroys an instance of a Sim SAT solver

Defined in SatSim.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

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

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

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

Defined in SatMinisat.c

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

Defined in SatMinisat.c

lsList 
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(
  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

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 lsList  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_without_groups(
  const SatIncSolver_ptr  solver, 
  const lsList  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

static void 
sat_sim_add(
  const SatSolver_ptr  solver, 
  const Be_Cnf_ptr  cnfProb, 
  SatSolverGroup  group 
)
Just stores all the clauses for later solving. This enables the use of 'add' and 'solve' interchangeably. Though this solution is not efficient. CNF formula must not be a constant!

Defined in SatSim.c

static int 
sat_sim_compare(
  lsGeneric  item1, 
  lsGeneric  item2 
)
Used to sort list of variable. Used in sat_sim_add only

Defined in SatSim.c

void 
sat_sim_deinit(
  SatSim_ptr  self 
)
Deinitializes SatSim object.

Defined in SatSim.c

static void 
sat_sim_finalize(
  Object_ptr  object, 
  void* dummy 
)
Sat Sim finalize method.

Defined in SatSim.c

void 
sat_sim_init(
  SatSim_ptr  self, 
  const char* name 
)
Initializes Sat Sim object.

Defined in SatSim.c

static lsList 
sat_sim_make_model(
  const SatSolver_ptr  self 
)
This function should never be invoked since the actual model is generated in 'solve' method

Defined in SatSim.c

static void 
sat_sim_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. CNF formula must not be a constant!

Defined in SatSim.c

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

Defined in SatSim.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

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

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

Defined in SatZchaff.c

lsList 
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

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 lsList  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_without_groups(
  const SatIncSolver_ptr  solver, 
  const lsList  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 2009/01/30 14h:53