SatMinisat.c
Routines related to SatMinisat object.
SatZchaff.c
Routines related to SatZchaff object.

SatMinisat.c

Routines related to SatMinisat object.

By: Andrei Tchaltsev, Marco Roveri

This file contains the definition of "SatMinisat" class. The solver contains its own coding of varibales, so input variables may by in any range from 1 .. INT_MAX, with possible holes in the range. Group Control: To control groups, every group has its ID, which is an usual internal variable. If a formula is added to a permanent group, then literals are just converted into the internal literals and the clauses are permamently added to the solver. If a formula is added to non-permanent group, then after convertion of literals, every clause in the group will additionally obtain one literal which is just group id, and then the clauses are added permanently to solver. Then if a group is turn on, then just its negated ID is added temporary to the solver. If we want to turn the group off, the just its ID is added temporary to the solver.

SatMinisat_create()
Creates a Minisat SAT solver and initializes it.
SatMinisat_destroy()
Destroys an instance of a MiniSat SAT solver
sat_minisat_cnfLiteral2minisatLiteral()
Convert a cnf literal into an internal literal used by minisat
sat_minisat_minisatLiteral2cnfLiteral()
Convert an internal minisat literal into a cnf literal
sat_minisat_add()
Adds a clause to the solver database.
sat_minisat_set_polarity()
Sets the polarity of the formula.
sat_minisat_set_preferred_variables()
Sets preferred variables in the solver
sat_minisat_clear_preferred_variables()
Clears preferred variables in the solver
sat_minisat_solve_all_groups()
Tries to solve all added formulas
sat_minisat_solve_permanent_group_assume()
Solves the permanent group under set of assumptions
sat_minisat_get_conflicts()
Returns set of conflicting assumptions
sat_minisat_make_model()
This function creates a model (in the original CNF variables)
sat_minisat_create_group()
Creates a new group and returns its ID
sat_minisat_destroy_group()
Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.
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_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_minisat_make_conflicts()
Obtains the set of conflicting assumptions from MiniSat
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_set_polarity_mode()
Pure virtual function, sets polarity mode accordingly to the passed value.
sat_minisat_get_polarity_mode()
Pure virtual function, returns currently set polarity mode.
sat_minisat_get_minisatClause()
Getter for minisatClause
sat_minisat_get_minisatClauseSize()
Getter for minisatClauseSize
sat_minisat_enlarge_minisatClause()
Enlarge minisatClause, adapt minisatClauseSize
sat_minisat_init()
Initializes Sat Minisat object.
sat_minisat_deinit()
Deinitializes SatMinisat object.
sat_minisat_finalize()
Finalize method of SatMinisat class.
_get_clause_size()
Computes the size of a clause.

SatZchaff.c

Routines related to SatZchaff object.

By: Andrei Tchaltsev, Marco Roveri

This file contains the definition of "SatZchaff" class. The solver contains its own coding of varibales, so input variables may by in any range from 1 .. INT_MAX, with possible holes in the range. Group Control: To control groups, every group has its ID, which is an usual internal variable. If a formula is added to a permanent group, then literals are just converted into the internal literals and the clauses are permamently added to the solver. If a formula is added to non-permanent group, then after convertion of literals, every clause in the group will additionally obtain one literal which is just group id, and then the clauses are added permanently to solver. Then if a group is turn on, then just its negated ID is added temporary to the solver. If we want to turn the group off, the just its ID is added temporary to the solver.

SatZchaff_create()
Creates a Zchaff SAT solver and initializes it.
SatZchaff_destroy()
Destroys a Zchaff SAT solver instence
sat_zchaff_cnfLiteral2zchaffLiteral()
Convert a cnf literal into an internal literal used by zchaff
sat_zchaff_zchaffLiteral2cnfLiteral()
Convert an internal zchaff literal into a cnf literal
sat_zchaff_add()
Adds a clause to the solver database.
sat_zchaff_set_polarity()
Sets the polarity of the formula.
sat_zchaff_set_preferred_variables()
Sets preferred variables in the solver
sat_zchaff_clear_preferred_variables()
Clears preferred variables in the solver
sat_zchaff_solve_all_groups()
Tries to solve all added formulas
sat_zchaff_solve_permanent_group_assume()
Solves the permanent group under set of assumptions
sat_zchaff_get_conflicts()
Returns set of conflicting assumptions
sat_zchaff_make_model()
This function creates a model (in the original cnf variables)
sat_zchaff_create_group()
Creates a new group and returns its ID
sat_zchaff_destroy_group()
Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.
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_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_make_conflicts()
Obtains the set of conflicting assumptions from zCahdd
sat_zchaff_init()
Initializes Sat Zchaff object.
sat_zchaff_deinit()
Deinitializes SatZchaff object.
sat_zchaff_finalize()
Finalize method of SatZchaff class.
_get_clause_size()
Computes the size of a clause.

Last updated on 2010/05/19 22h:26