SatMinisat.c
SatZchaff.c
By: Andrei Tchaltsev, Marco Roveri, Marco Pensallorto
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()
SatMinisat_destroy()
sat_minisat_cnfLiteral2minisatLiteral()
sat_minisat_minisatLiteral2cnfLiteral()
sat_minisat_add()
sat_minisat_set_polarity()
sat_minisat_set_preferred_variables()
sat_minisat_clear_preferred_variables()
sat_minisat_solve_all_groups()
sat_minisat_solve_permanent_group_assume()
sat_minisat_get_conflicts()
sat_minisat_make_model()
sat_minisat_create_group()
sat_minisat_destroy_group()
sat_minisat_move_to_permanent_and_destroy_group()
sat_minisat_solve_groups()
sat_minisat_solve_without_groups()
sat_minisat_make_conflicts()
sat_minisat_set_random_mode()
sat_minisat_set_polarity_mode()
sat_minisat_get_polarity_mode()
sat_minisat_get_minisatClause()
sat_minisat_get_minisatClauseSize()
sat_minisat_enlarge_minisatClause()
sat_minisat_curr_itp_group()
sat_minisat_new_itp_group()
sat_minisat_extract_interpolant()
sat_minisat_init()
sat_minisat_deinit()
sat_minisat_finalize()
_get_clause_size()
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()
SatZchaff_destroy()
sat_zchaff_cnfLiteral2zchaffLiteral()
sat_zchaff_zchaffLiteral2cnfLiteral()
sat_zchaff_add()
sat_zchaff_set_polarity()
sat_zchaff_set_preferred_variables()
sat_zchaff_clear_preferred_variables()
sat_zchaff_solve_all_groups()
sat_zchaff_solve_permanent_group_assume()
sat_zchaff_get_conflicts()
sat_zchaff_make_model()
sat_zchaff_create_group()
sat_zchaff_destroy_group()
sat_zchaff_move_to_permanent_and_destroy_group()
sat_zchaff_solve_groups()
sat_zchaff_solve_without_groups()
sat_zchaff_make_conflicts()
sat_zchaff_init()
sat_zchaff_deinit()
sat_zchaff_finalize()
_get_clause_size()