-
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