SatMinisat_create()
Creates a Minisat SAT solver and initializes it.
SatMinisat_destroy()
Destroys an instance of a MiniSat SAT solver
SatZchaff_create()
Creates a Zchaff SAT solver and initializes it.
SatZchaff_destroy()
Destroys a Zchaff SAT solver instence
_get_clause_size()
Computes the size of a clause.
_get_clause_size()
Computes the size of a clause.
sat_minisat_add()
Adds a clause to the solver database.
sat_minisat_clear_preferred_variables()
Clears preferred variables in the solver
sat_minisat_cnfLiteral2minisatLiteral()
Convert a cnf literal into an internal literal used by minisat
sat_minisat_create_group()
Creates a new group and returns its ID
sat_minisat_deinit()
Deinitializes SatMinisat object.
sat_minisat_destroy_group()
Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.
sat_minisat_enlarge_minisatClause()
Enlarge minisatClause, adapt minisatClauseSize
sat_minisat_finalize()
Finalize method of SatMinisat class.
sat_minisat_get_conflicts()
Returns set of conflicting assumptions
sat_minisat_get_minisatClauseSize()
Getter for minisatClauseSize
sat_minisat_get_minisatClause()
Getter for minisatClause
sat_minisat_get_polarity_mode()
Pure virtual function, returns currently set polarity mode.
sat_minisat_init()
Initializes Sat Minisat object.
sat_minisat_make_conflicts()
Obtains the set of conflicting assumptions from MiniSat
sat_minisat_make_model()
This function creates a model (in the original CNF variables)
sat_minisat_minisatLiteral2cnfLiteral()
Convert an internal minisat literal into a cnf literal
sat_minisat_move_to_permanent_and_destroy_group()
Moves all formulas from a group into the permanent group of the solver and then destroy the given group.
sat_minisat_set_polarity_mode()
Pure virtual function, sets polarity mode accordingly to the passed value.
sat_minisat_set_polarity()
Sets the polarity of the formula.
sat_minisat_set_preferred_variables()
Sets preferred variables in the solver
sat_minisat_set_random_mode()
Pure virtual function, sets random polarity mode if seed is not zero, otherwise sets default non-random polarity mode.
sat_minisat_solve_all_groups()
Tries to solve all added formulas
sat_minisat_solve_groups()
Tries to solve formulas from the groups in the list.
sat_minisat_solve_permanent_group_assume()
Solves the permanent group under set of assumptions
sat_minisat_solve_without_groups()
Tries to solve formulas in groups belonging to the solver except the groups in the list.
sat_zchaff_add()
Adds a clause to the solver database.
sat_zchaff_clear_preferred_variables()
Clears preferred variables in the solver
sat_zchaff_cnfLiteral2zchaffLiteral()
Convert a cnf literal into an internal literal used by zchaff
sat_zchaff_create_group()
Creates a new group and returns its ID
sat_zchaff_deinit()
Deinitializes SatZchaff object.
sat_zchaff_destroy_group()
Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.
sat_zchaff_finalize()
Finalize method of SatZchaff class.
sat_zchaff_get_conflicts()
Returns set of conflicting assumptions
sat_zchaff_init()
Initializes Sat Zchaff object.
sat_zchaff_make_conflicts()
Obtains the set of conflicting assumptions from zCahdd
sat_zchaff_make_model()
This function creates a model (in the original cnf variables)
sat_zchaff_move_to_permanent_and_destroy_group()
Moves all formulas from a group into the permanent group of the solver and then destroy the given group.
sat_zchaff_set_polarity()
Sets the polarity of the formula.
sat_zchaff_set_preferred_variables()
Sets preferred variables in the solver
sat_zchaff_solve_all_groups()
Tries to solve all added formulas
sat_zchaff_solve_groups()
Tries to solve formulas from the groups in the list.
sat_zchaff_solve_permanent_group_assume()
Solves the permanent group under set of assumptions
sat_zchaff_solve_without_groups()
Tries to solve formulas in groups belonging to the solver except the groups in the list.
sat_zchaff_zchaffLiteral2cnfLiteral()
Convert an internal zchaff literal into a cnf literal

Last updated on 2011/04/06 21h:16