sim.h
External header file
simInt.h
Internal header file
simClause.c
Primitives for clauses.
simCons.c
Consistency checking routines.
simData.c
Data structure handling.
simError.c
Error handling
simHeur.c
Search heuristics.
simLookAhead.c
A compendium of lookahead techniques.
simLookBack.c
A compendium of look back techniques.
simMemory.c
Memory handling
simOutput.c
Output routines.
simParse.c
Parsing routines.
simProp.c
Primitives for propositions
simSolve.c
DLL algorithm
simTime.c
Timers handling
simTrace.c
Running trace handling

sim.h

External header file

By: Armando Tacchella Davide Zambonin


simInt.h

Internal header file

By: Armando Tacchella Davide Zambonin

()
Decides what kind of consistency check is to be performed.
()
Selects how to propagate the proposition.
()
Selects how to propagate the proposition.
()
Calls the selected heuristics.
()
Selects the backtracking function.
()
When to call MLF.
()
Tests if the clause is open.
()
Checks if a solution is found.
()
Swaps two scalars.
()
Return the absolute value of an integer.
()
Bit annotarion in proposition pointers.
()
Remove a clause.
()
Sim memory checking macro.
()
Returns a long integer in the range [0, x-1
()
Stores the random generation seed.
()
Increments a statistic.
()
Adds a given number to a statistic.
()
Decrements a statistic.
()
Updates a (maximum) statistic.
()
Updates a (minimum) statistic.
()
Sim `assert' macro.
()
Sim trace enabler.
()
Prints a message about a split.
()
Prints a message about an heuristics choice.
()
Prints a message about an implied assignment.
()
Prints a message about retracting a valuation.
()
Prints a message about a skipped choice point.
()
Prints a message about a contradiction.
()
Prints a message about the creation of a new working reason.
()
Prints a message about the current working reason.
()
Prints a message about learning a clause.

simClause.c

Primitives for clauses.

By: Armando Tacchella

Internal procedures included in this module:

See Alsosim.h

SimClauseInit()
Initializes a clause.
SimClauseClear()
Clears a clause.

simCons.c

Consistency checking routines.

By: Armando Tacchella Davide Zambonin

External procedures included in this module:

See AlsosimSolve.c

SimDllGetModels()
Consistency checkingl.
SimDllGetModelsHorn()
Consistency checking with horn relaxation.

simData.c

Data structure handling.

By: Armando Tacchella Davide Zambonin

External procedures included in this module:

Internal procedures included in this module:

Sim_ParamInit()
Creates a default parameter setup as follows:
Idx Default value Parameter Notes -------------------------------------------------------------- 0 unlimited SIM_TIMEOUT seconds 1 unlimited SIM_MEMOUT megabytes 2 SIM_BOEHM_HEUR SIM_HEURISTICS 0..SIM_HEUR_NUM 3 1 SIM_SOL_NUM N >= 1 4 3 SIM_LEARN_ORDER N >= 2 5 SIM_RELEVANCE SIM_LEARN_TYPE SIM_RELEVANCE/SIM_SIZE 6 0 SIM_MODEL_PROPS 0/1 7 SIM_NONE SIM_PPROC_STRENGTH 0..SIM_RESOLVE 8 0 SIM_RND_SEED N >= 0 9 0 SIM_VERBOSITY 0/1 10 0 SIM_HEUR_PARAM N >= 0 11 100 SIM_MAX_VAR_NUM N > 1 12 1000 SIM_MAX_CL_NUM N > 1 -------------------------------------------------------------- Notice that the actual number of variables and clauses in the formula *cannot* be greater than SIM_MAX_VAR_NUM and SIM_MAX_CL_NUM respectively. Failing to dimension these parameters correctly will cause the solver to crash.
Sim_ParamSet()
Changes the value of a specific parameter.
Sim_DllInit()
Initialize the DLL module. The array `params' must be suitably initialized.
Sim_DllNewCl()
Create a new (empty) clause and return its unique id (an integer code greater than or equal to 0). Trying to add a new clause without committing any pending one yields -1 as a return value.
Sim_DllNewClSize()
Create a new (empty) clause and return its unique id, (an integer code greater than or equal to 0). The clause is dimensioned to accomodate `size' literals without reallocations. Trying to add a new clause without committing any pending one yields -1 as a return value.
Sim_DllAddLit()
Add a literal `lit' to the current clause. `lit' must be an integer such that its absolute value is greater than 0 and smaller than or equal to the biggest allowed variable index. A positive (negative) integer denotes a positive (negative) occurrence of the corresponding variable. If `lit' does not fulfill the above conditions, or if there is no pending clause to add `lit' to, -1 is returned. The function returns 0 if the pending clause becomes tautologous, and 1 otherwise. Redundant literals are always discarded.
Sim_DllCommitCl()
Commit the pending clause. If there is no such clause, or the given `clId' is differente from the current one, -1 is returned. If the committed clause is empty, 0 is returned and the function resets the state (no pending clause). On success, `clId' is returned.
Sim_DllPropMakeIndep()
State model membership, i.e., a proposition that is not dependent or defined. 'prop` must be a positive non-zero integer smaller than or equal to the biggest allowed variable index.
Sim_DllGetSolution()
Get the current assignment to propositions. The returned object is an array of integers indexed on propositions. For each proposition, the values SIM_TT, SIM_FF, SIM_DC are given, meaning that the proposition was assigned to true, false or not assigned at all (Don't Care). Propositions that did not occur in the formula receive a default value of SIM_DC. The first location of the returned array contains the biggest proposition index.
Sim_DllGetStack()
Get the current search stack contents. The returned object is an array representing truth assignment to propositions encoded as literals (negative value if the proposition was assigned to false and vice versa). The first location of the returned array is the cardinality of the truth assignment.
Sim_DllClear()
Destroys the internal data structure.
SimDllBuild()
Final build of the data structure.
SimDllInsProp()
Inserts a new proposition in the DLL data structure.
SimDllDelProp()
Removes a literal from the DLL data structure.

simError.c

Error handling

By: Armando Tacchella Davide Zambonin

Internal procedures included in this module:

Sim_GetErrorCode()
Returns the error code (if any).
Sim_GetErrorLocation()
Returns the error location (if any).
SimDllThrow()
Prompts an error to the user and raises a SIGUSR1.

simHeur.c

Search heuristics.

By: Armando Tacchella Davide Zambonin

External procedures included in this module:

See AlsosimSolve.c

()
Assigns a truth value to a proposition and propagates it throughout the formula doing unit resolutions only.
()
Empty macro.
()
Empty macro.
()
Increments the unit counter (unit).
()
Increments the unit counter (unit).
()
Increments the unit counter (unit).
()
Store q reason.
()
Performs unit propagation.
()
Set the flags that witness an assignment.
()
Resets propagations.
()
Unassigns all the propositions in changedProps. Restores the number of open propositions to the old value in the changed clauses. Computes working reason while restoring the counters.
SimDllUsrHeur()
Asks the user for a literal.
SimDllRndHeur()
Selects an open literal randomly
SimDllJWHeur()
Chooses the best literal with Jeroslow-Wang's heuristics.
SimDll2JWHeur()
Chooses the best literal according to 2-sided JW.
SimDllBoehmHeur()
Choose the best literal according to Boehm's heuristics.
SimDllMomsHeur()
Chooses the best literal according to M.O.M.S. heuristics.
SimDllInitSatzHeur()
Allocate auxiliary data for Chu Min Li heuristics.
SimDllEndSatzHeur()
Free auxiliary data for Chu Min Li heuristics.
SimDllSatzHeur()
Choose the best literal according to Satz heuristics.
SimDllInitSatoHeur()
Allocate auxiliary data for Sato 3.2 heuristics.
SimDllEndSatoHeur()
Free auxiliary data for Sato heuristics.
SimDllSatoHeur()
Choose the best literal according to Sato 3.2 heuristics.
SimDllInitRelsatHeur()
Allocate auxiliary data for Relsat heuristics.
SimDllEndRelsatHeur()
Free auxiliary data for Relsat heuristics.
SimDllRelsatHeur()
Chooses the best literal according to Relsat 2.0 heuristics.
SimDllInitUnitieHeur()
Allocate auxiliary data for Unitie heuristics.
SimDllEndUnitieHeur()
Free auxiliary data for Unitie heuristics.
SimDllUnitieHeur()
A simple unit based heuristics with tie breaking.
DllMomsHeur()
Chooses the best literal according to M.O.M.S. heuristics.
Examine()
Evaluates how much an assignment reduces the formula.
Examine0()
Evaluates how much an assignment reduces the formula.
Propagate()
Evaluates how much an assignment reduces the formula.
CountBinaryPos()
Evaluates how many times a propositions occurres in a binary clause.
CountBinaryNeg()
Evaluates how many times a propositions occurres in a binary clause.
CountNoBinaryPos()
Calculate a score for a proposition.
CountNoBinaryNeg()
Calculate a score for a proposition.

simLookAhead.c

A compendium of lookahead techniques.

By: Armando Tacchella Davide Zambonin

Internal procedures included in this module:

See AlsosimSolve.c

SimDllBcp()
Performs Boolean Constraint Propagation (Unit resolution)
SimDllMlf()
Performs Monotone Literal Fixing (Pure literal).

simLookBack.c

A compendium of look back techniques.

By: Armando Tacchella Davide Zambonin

Internal procedures included in this module:

See AlsosimSolve.c

SimDllChronoBt()
Stackwise chronological backtracking.
SimDllBackjumping()
Stackwise conflict directed backjumping.
SimDllInitWr()
Initializes the working reason.
SimDllResolveWithWr()
Resolves the given clause with the working reason.
SimDllMakeClauseFromWr()
Creates a clause from the working reason.
SimDllLearnClause()
Learns a clause.
SimDllUnlearnClause()
Delete clause from learned clauses database.

simMemory.c

Memory handling

By: Armando Tacchella

Internal procedures included in this module:

See Alsosim.h

SimDllStartMemory()
Starts memory accounting.
SimDllStopMemory()
Stops memory accounting.
SimDllSetMemout()
Sets the memeout on the process.

simOutput.c

Output routines.

By: Armando Tacchella Davide Zambonin

External procedures included in this module:

Internal procedures included in this module:

See AlsosimSolve.c

Sim_DllPrintFormulaDimacs()
Print the formula in the DLL module using DIMACS format.
Sim_DllPrintModel()
Print the model.
Sim_DllPrintStats()
Prints internal statistics.
Sim_DllPrintTimers()
Prints internal timers.
Sim_DllPrintResult()
Prints the result (formatted).
Sim_DllPrintParams()
Prints parameters (configuration).
SimDllPrintStack()
Print the search stack.
SimDllPrintPath()
Print the search path.
SimDllPrintOpen()
Print the open propositions.
SimDllPrintFormulaStruct()
Print the formula in the DLL module showing internal status.
SimDllPrintLearnedFW()
Prints learned clauses (first learned, first printed).
SimDllPrintLearnedBW()
Prints learned clauses (last learned, first printed).
SimDllPrintClause()
Prints a clause structure.

simParse.c

Parsing routines.

By: Armando Tacchella Davide Zambonin

External procedure included in this module:

Internal procedures included in this module: SeeAlso [simData.c

Sim_DllParseDimacs()
Parses a DIMACS cnf problem file into a DLL module.
SimDllParseDimacsCls()
Parses clauses from a DIMACS file.

simProp.c

Primitives for propositions

By: Armando Tacchella

Internal procedures included in this module:

See Alsosim.h

SimPropInit()
Initializes a proposition.
SimPropClear()
Clears a proposition.

simSolve.c

DLL algorithm

By: Armando Tacchella Davide Zambonin

External procedures included in this module:

Internal procedures included in this module:

See AlsosimHeur.c simLookAhead.c simLookBack.c simCons.c

Sim_DllSolve()
Solves a formula using the Davis-Logemann-Loveland algorithm.
SimDllExtendPropTT()
Valuates a proposition to SIM_TT
SimDllExtendPropFF()
Valuates a proposition to SIM_FF
SimDllRetractPropTT()
Unvaluates a proposition (assigned to SIM_TT)
SimDllRetractPropFF()
Unvaluates a proposition (assigned to SIM_FF)
SimDllCheck()
Checks a solution found by Sim_DllSolve.

simTime.c

Timers handling

By: Armando Tacchella

Internal procedures included in this module:

See Alsosim.h

SimDllStartTimer()
Starts a timer.
SimDllStopTimer()
Stops a timer.
SimDllSetTimeout()
Sets the timeout on the process.

simTrace.c

Running trace handling

By: Armando Tacchella

Internal procedures included in this module:

SimDllTraceNodes()
Tracing search nodes.
SimDllTraceLeafs()
Tracing search leafs.

Last updated on 2009/03/04 12h:51