SatMinisat_create()
Creates a Minisat SAT solver and initializes it.
SatMinisat_destroy()
Destroys an instance of a MiniSat SAT solver
SatSim_create()
Creates a Sim SAT solver and initializes it.
SatSim_destroy()
Destroys an instance of a Sim SAT solver
SatZchaff_create()
Creates a Zchaff SAT solver and initializes it.
SatZchaff_destroy()
Destroys a Zchaff SAT solver instence
sat_minisat_add()
Adds a clause to the solver database.
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_finalize()
Finalize method of SatMinisat class.
sat_minisat_init()
Initializes Sat Minisat object.
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()
Sets the polarity of the formula.
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_without_groups()
Tries to solve formulas in groups belonging to the solver except the groups in the list.
sat_sim_add()
Adds a clause to the solver database.
sat_sim_compare()
Compares two variables indexes
sat_sim_deinit()
Deinitializes SatSim object.
sat_sim_finalize()
Sat Sim finalize method.
sat_sim_init()
Initializes Sat Sim object.
sat_sim_make_model()
This function should never be invoked since the actual model is generated in 'solve' method
sat_sim_set_polarity()
Sets the polarity of the formula.
sat_sim_solve_all_groups()
Tries to solve all added formulas
sat_zchaff_add()
Adds a clause to the solver database.
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_init()
Initializes Sat Zchaff object.
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_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_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 2009/01/30 15h:04