-
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:
- SimClauseInit() clause construtor
- SimClauseClear() clause destructor
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:
- SimDllGetModels() checks if the
number of open clauses is zero. If so, decrements
the number of solutions to find;
- SimDllGetModelsHorn() checks if the
number of open non-horn clauses is zero. If so,
decrements the number of solutions to find.
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:
- constructors, destructors, etc.
- Sim_DllInit() initializes the dll module;
- Sim_DllClear() shuts down the dll module;
- adding clauses (tautologies are *always* discarded,
duplicated literals are *always* removed):
- Sim_DllNewCl() adds a new (empty) clause;
- Sim_DllNewClSize() sets the size
- Sim_DllAddLit() adds literals to the clause;
- Sim_DllCommitCl() commits the clause;
- other interface elements:
- Sim_DllPropIsModel() states model membership
- Sim_DllGetSolution() gets the solution
- Sim_DllGetStack() gets the stack contents
Internal procedures included in this module:
- SimDllBuild() completes the initialization;
- SimDllInsProp() adds a proposition;
- SimDllDelProp() removes a proposition.
-
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:
- SimDllThrow() raises a SIG_USR1 to signal
that something was wrong
-
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:
- SimDllUsrHeur() prompts the user
- SimDllRndHeur() chooses a literal randomly;
- SimDllJWHeur() classical Jeroslow-Wang;
- SimDll2JWHeur() two-sided Jeroslow-Wang;
- SimDllBoehmHeur() Boehm heuristics;
- SimDllMomsHeur() Moms heuristics;
- SimDllInitSatzHeur()
- SimDllSatzHeur() Satz heuristics;
- SimDllEndSatzHeur()
- SimDllInitSatoHeur()
- SimDllSatoHeur() Sato 3.2 heuristics;
- SimDllEndSatoHeur()
- SimDllInitRelsatHeur()
- SimDllRelsatHeur() Relsat 2.0 heuristics;
- SimDllEndRelsatHeur()
- SimDllInitUnitieHeur()
- SimDllUnitieHeur() Simple unit based
- SimDllEndUnitieHeur()
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:
- SimDllBcp() performs Binary Constraint Propagation;
- SimDllMlf() performs Monotone Literal Fixing.
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:
- SimDllChronoBt() performs stackwise chronological
backtracking
- SimDllBackjumping() performs non-chronological
dependency directed backtracking
- SimDllInitWr()
- SimDllResolveWithWr()
- SimDllMakeClFromWr()
- SimDllLearnClause()
- SimDllUnlearnClause()
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:
- SimDllStartMemory() begin memory accounting
- SimDllStopMemory() end memory accounting
- SimDllSetMemout() sets the memory-out
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:
- Sim_DllPrintFormulaDimacs() prints out the
internal formula in DIMACS syntax;
- Sim_DllPrintModel() prints out the current
truth assignment;
- Sim_DllPrintStats() prints out statistics.
- Sim_DllPrintTimers() prints out timers.
- Sim_DllPrintResult() prints out a formatted result
- Sim_DllPrintParam() prints out parameters.
Internal procedures included in this module:
- SimDllPrintStack() prints out the search stack;
- SimDllPrintPath() prints out the search path;
- SimDllPrintOpen() prints out the open variables.
- SimDllPrintStruct() prints formula structure;
- SimDllPrintClause prints out a clause;
- SimDllPrintLearnedFW prints learned clauses (FIFO);
- SimDllPrintLearnedBW prints learned clauses (LIFO).
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:
- Sim_DllParseDimacsFile() parses a DIMACS
cnf problem file;
Internal procedures included in this module:
- SimDllParseDimacsCls() parses a set of
clauses in DIMACS format;
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:
- SimPropInit() proposition construtor
- SimPropClear() proposition destructor
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:
- Sim_DllSolve() the main DLL routine
Internal procedures included in this module:
- SimDllExtendProp() propagates a truth value;
- SimDllRetractProp() undoes the effects of a
propagation.
- SimDllCheck() solution checking
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:
- SimDllStartTimer() starts a timer
- SimDllStopTimer() stops a timer
- SimDllSetTimout() sets the timeout
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 tree nodes
(heuristics choices)
- SimDllTraceLeafs() Tracing search tree leafs
(backtracks)
-
SimDllTraceNodes()
- Tracing search nodes.
-
SimDllTraceLeafs()
- Tracing search leafs.
Last updated on 2009/03/04 12h:51