SatMinisat_ptr
SatMinisat_create(
const char* name
)
- The first parameter is the name of the solver.
- Defined in
SatMinisat.c
void
SatMinisat_destroy(
SatMinisat_ptr self
)
- Destroys an instance of a MiniSat SAT solver
- Defined in
SatMinisat.c
SatSim_ptr
SatSim_create(
const char* name
)
- The first parameter is the name of the solver.
- Defined in
SatSim.c
void
SatSim_destroy(
SatSim_ptr self
)
- Destroys an instance of a Sim SAT solver
- Defined in
SatSim.c
SatZchaff_ptr
SatZchaff_create(
const char* name
)
- The first parameter is the name of the solver.
- Defined in
SatZchaff.c
void
SatZchaff_destroy(
SatZchaff_ptr self
)
- The first parameter is the name of the solver.
- Defined in
SatZchaff.c
void
sat_minisat_add(
const SatSolver_ptr solver,
const Be_Cnf_ptr cnfProb,
SatSolverGroup group
)
- converts all CNF literals into the internal literals,
adds a group id to every clause (if group is not permament) and then add
obtained clauses to actual Minisat
- Defined in
SatMinisat.c
int
sat_minisat_cnfLiteral2minisatLiteral(
SatMinisat_ptr self,
int cnfLiteral
)
- The literal may not be 0 (because 0 cannot have sign).
First, the function obtains the cnf variable (removes the sign),
obtains associated internal var through hash table(creates if necessary
an internal variable)
and then converts it in minisat literal (just adjust the sign).
If necessary a new minisat variable is created.
- See Also
sat_minisat_minisatLiteral2cnfLiteral
- Defined in
SatMinisat.c
SatSolverGroup
sat_minisat_create_group(
const SatIncSolver_ptr solver
)
- Adds the group at the END of the existing groups list
- See Also
SatIncSolver_destroy_group
SatIncSolver_move_to_permanent_and_destroy_group
- Defined in
SatMinisat.c
void
sat_minisat_deinit(
SatMinisat_ptr self
)
- Deinitializes SatMinisat object.
- Defined in
SatMinisat.c
void
sat_minisat_destroy_group(
const SatIncSolver_ptr solver,
SatSolverGroup group
)
- Just adds to the solver a unit clause with positive literal
of a variable with index equal to group id
- See Also
SatIncSolver_create_group
- Defined in
SatMinisat.c
static void
sat_minisat_finalize(
Object_ptr object,
void* dummy
)
- Pure virtual function. This must be refined by derived classes.
- Defined in
SatMinisat.c
void
sat_minisat_init(
SatMinisat_ptr self,
const char* name
)
- Initializes Sat Minisat object.
- Defined in
SatMinisat.c
lsList
sat_minisat_make_model(
const SatSolver_ptr solver
)
- The previous invocation of SAT_Solve should have been successful
- Defined in
SatMinisat.c
int
sat_minisat_minisatLiteral2cnfLiteral(
SatMinisat_ptr self,
int minisatLiteral
)
- The variable in the literal has to be created by
sat_minisat_cnfLiteral2minisatLiteral only.
First, the function obtains the minisat variable from the literal,
obtains associated cnf variable (there must already be the association),
and then converts it in cnf literal (adjust the sign)
- See Also
sat_minisat_cnfLiteral2minisatLiteral
- Defined in
SatMinisat.c
void
sat_minisat_move_to_permanent_and_destroy_group(
const SatIncSolver_ptr solver,
SatSolverGroup group
)
- just adds to minisat a unit clause with negative literal
of a variable with index equal to group id
- See Also
SatIncSolver_create_group
SatSolver_get_permanent_group
- Defined in
SatMinisat.c
void
sat_minisat_set_polarity(
const SatSolver_ptr solver,
const Be_Cnf_ptr cnfProb,
int polarity,
SatSolverGroup group
)
- Sets the polarity of the formula.
Polarity 1 means the formula is considered as positive, and -1 means
the negation of the formula will be solved.
A unit clause of the literal (with sign equal to polarity)
corresponding to the given CNF formula is added to the solve.
- Defined in
SatMinisat.c
SatSolverResult
sat_minisat_solve_all_groups(
const SatSolver_ptr solver
)
- Tries to solve all added formulas
- Defined in
SatMinisat.c
SatSolverResult
sat_minisat_solve_groups(
const SatIncSolver_ptr solver,
const lsList groups
)
- The permanent group is automatically added to the list.
Returns a flag whether the solving was successful. If it was successful only
then SatSolver_get_model may be invoked to obtain the model
- Defined in
SatMinisat.c
SatSolverResult
sat_minisat_solve_without_groups(
const SatIncSolver_ptr solver,
const lsList groups
)
- The permanent group must not be in the list.
Returns a flag whether the solving was successful. If it was successful only
then SatSolver_get_model may be invoked to obtain the model
- See Also
SatSolverResult
SatSolver_get_permanent_group
SatIncSolver_create_group
SatSolver_get_model
- Defined in
SatMinisat.c
static void
sat_sim_add(
const SatSolver_ptr solver,
const Be_Cnf_ptr cnfProb,
SatSolverGroup group
)
- Just stores all the clauses for later solving. This enables the use
of 'add' and 'solve' interchangeably. Though this solution is not efficient.
CNF formula must not be a constant!
- Defined in
SatSim.c
static int
sat_sim_compare(
lsGeneric item1,
lsGeneric item2
)
- Used to sort list of variable. Used in sat_sim_add only
- Defined in
SatSim.c
void
sat_sim_deinit(
SatSim_ptr self
)
- Deinitializes SatSim object.
- Defined in
SatSim.c
static void
sat_sim_finalize(
Object_ptr object,
void* dummy
)
- Sat Sim finalize method.
- Defined in
SatSim.c
void
sat_sim_init(
SatSim_ptr self,
const char* name
)
- Initializes Sat Sim object.
- Defined in
SatSim.c
static lsList
sat_sim_make_model(
const SatSolver_ptr self
)
- This function should never be invoked since
the actual model is generated in 'solve' method
- Defined in
SatSim.c
static void
sat_sim_set_polarity(
const SatSolver_ptr solver,
const Be_Cnf_ptr cnfProb,
int polarity,
SatSolverGroup group
)
- Sets the polarity of the formula.
Polarity 1 means the formula is considered as positive, and -1 means
the negation of the formula will be solved.
CNF formula must not be a constant!
- Defined in
SatSim.c
static SatSolverResult
sat_sim_solve_all_groups(
const SatSolver_ptr solver
)
- Tries to solve all added formulas
- Defined in
SatSim.c
void
sat_zchaff_add(
const SatSolver_ptr solver,
const Be_Cnf_ptr cnfProb,
SatSolverGroup group
)
- converts all CNF literals into the internal literals,
adds a group id to every clause (if group is not permament) and then add
obtained clauses to actual ZChaff
- Defined in
SatZchaff.c
int
sat_zchaff_cnfLiteral2zchaffLiteral(
SatZchaff_ptr self,
int cnfLiteral
)
- The literal may not be 0 (because 0 cannot have sign).
First, the function obtains the cnf variable (removes the sign),
obtains associated internal var through hash table(creates if necessary
an internal variable)
and then converts it in zchaff literal (var*2+sign, see ZChaff SAT.h).
If necessary a new minisat variable is created.
- See Also
sat_zchaff_zchaffLiteral2cnfLiteral
- Defined in
SatZchaff.c
SatSolverGroup
sat_zchaff_create_group(
const SatIncSolver_ptr solver
)
- Adds the group at the END of the existing groups list
- See Also
SatIncSolver_destroy_group
SatIncSolver_move_to_permanent_and_destroy_group
- Defined in
SatZchaff.c
void
sat_zchaff_deinit(
SatZchaff_ptr self
)
- Deinitializes SatZchaff object.
- Defined in
SatZchaff.c
void
sat_zchaff_destroy_group(
const SatIncSolver_ptr solver,
SatSolverGroup group
)
- Just adds to the solver a unit clause with positive literal
of a variable with index equal to group id
- See Also
SatIncSolver_create_group
- Defined in
SatZchaff.c
static void
sat_zchaff_finalize(
Object_ptr object,
void* dummy
)
- Pure virtual function. This must be refined by derived classes.
- Defined in
SatZchaff.c
void
sat_zchaff_init(
SatZchaff_ptr self,
const char* name
)
- Initializes Sat Zchaff object.
- Defined in
SatZchaff.c
lsList
sat_zchaff_make_model(
const SatSolver_ptr solver
)
- The previous invocation of SAT_Solve should have been successful
- Defined in
SatZchaff.c
void
sat_zchaff_move_to_permanent_and_destroy_group(
const SatIncSolver_ptr solver,
SatSolverGroup group
)
- just adds to zchaff a unit clause with negative literal
of a variable with index equal to group id
- See Also
SatIncSolver_create_group
SatSolver_get_permanent_group
- Defined in
SatZchaff.c
void
sat_zchaff_set_polarity(
const SatSolver_ptr solver,
const Be_Cnf_ptr cnfProb,
int polarity,
SatSolverGroup group
)
- Sets the polarity of the formula.
Polarity 1 means the formula is considered as positive, and -1 means
the negation of the formula will be solved.
A unit clause of the literal (with sign equal to polarity)
corresponding to the given CNF formula is added to the solve.
- Defined in
SatZchaff.c
SatSolverResult
sat_zchaff_solve_all_groups(
const SatSolver_ptr solver
)
- Tries to solve all added formulas
- Defined in
SatZchaff.c
SatSolverResult
sat_zchaff_solve_groups(
const SatIncSolver_ptr solver,
const lsList groups
)
- The permanent group is automatically added to the list.
Returns a flag whether the solving was successful. If it was successful only
then SatSolver_get_model may be invoked to obtain the model
- Defined in
SatZchaff.c
SatSolverResult
sat_zchaff_solve_without_groups(
const SatIncSolver_ptr solver,
const lsList groups
)
- The permanent group must not be in the list.
Returns a flag whether the solving was successful. If it was successful only
then SatSolver_get_model may be invoked to obtain the model
- See Also
SatSolverResult
SatSolver_get_permanent_group
SatIncSolver_create_group
SatSolver_get_model
- Defined in
SatZchaff.c
int
sat_zchaff_zchaffLiteral2cnfLiteral(
SatZchaff_ptr self,
int zchaffLiteral
)
- The variable in the literal has to be created by
sat_zchaff_cnfLiteral2zchaffLiteral only.
First, the function obtains the zchaff variable from the literal,
obtains associated cnf variable (there must already be the association),
and then converts it in cnf literal (add the sign)
- See Also
sat_zchaff_cnfLiteral2zchaffLiteral
- Defined in
SatZchaff.c