-
CountBinaryNeg()
- Evaluates how many times a propositions occurres in a
binary clause.
-
CountBinaryPos()
- Evaluates how many times a propositions occurres in a
binary clause.
-
CountNoBinaryNeg()
- Calculate a score for a proposition.
-
CountNoBinaryPos()
- Calculate a score for a proposition.
-
DllMomsHeur()
- Chooses the best literal according to M.O.M.S. heuristics.
-
Examine0()
- Evaluates how much an assignment reduces the formula.
-
Examine()
- Evaluates how much an assignment reduces the formula.
-
Propagate()
- Evaluates how much an assignment reduces the formula.
-
SimClauseClear()
- Clears a clause.
-
SimClauseInit()
- Initializes a clause.
-
SimDll2JWHeur()
- Chooses the best literal according to 2-sided JW.
-
SimDllBackjumping()
- Stackwise conflict directed backjumping.
-
SimDllBcp()
- Performs Boolean Constraint Propagation (Unit resolution)
-
SimDllBoehmHeur()
- Choose the best literal according to Boehm's heuristics.
-
SimDllBuild()
- Final build of the data structure.
-
SimDllCheck()
- Checks a solution found by Sim_DllSolve.
-
SimDllChronoBt()
- Stackwise chronological backtracking.
-
SimDllDelProp()
- Removes a literal from the DLL data structure.
-
SimDllEndRelsatHeur()
- Free auxiliary data for Relsat heuristics.
-
SimDllEndSatoHeur()
- Free auxiliary data for Sato heuristics.
-
SimDllEndSatzHeur()
- Free auxiliary data for Chu Min Li heuristics.
-
SimDllEndUnitieHeur()
- Free auxiliary data for Unitie heuristics.
-
SimDllExtendPropFF()
- Valuates a proposition to SIM_FF
-
SimDllExtendPropTT()
- Valuates a proposition to SIM_TT
-
SimDllGetModelsHorn()
- Consistency checking with horn relaxation.
-
SimDllGetModels()
- Consistency checkingl.
-
SimDllInitRelsatHeur()
- Allocate auxiliary data for Relsat heuristics.
-
SimDllInitSatoHeur()
- Allocate auxiliary data for Sato 3.2 heuristics.
-
SimDllInitSatzHeur()
- Allocate auxiliary data for Chu Min Li heuristics.
-
SimDllInitUnitieHeur()
- Allocate auxiliary data for Unitie heuristics.
-
SimDllInitWr()
- Initializes the working reason.
-
SimDllInsProp()
- Inserts a new proposition in the DLL data structure.
-
SimDllJWHeur()
- Chooses the best literal with Jeroslow-Wang's heuristics.
-
SimDllLearnClause()
- Learns a clause.
-
SimDllMakeClauseFromWr()
- Creates a clause from the working reason.
-
SimDllMlf()
- Performs Monotone Literal Fixing (Pure literal).
-
SimDllMomsHeur()
- Chooses the best literal according to M.O.M.S. heuristics.
-
SimDllParseDimacsCls()
- Parses clauses from a DIMACS file.
-
SimDllPrintClause()
- Prints a clause structure.
-
SimDllPrintFormulaStruct()
- Print the formula in the DLL module showing internal status.
-
SimDllPrintLearnedBW()
- Prints learned clauses (last learned, first printed).
-
SimDllPrintLearnedFW()
- Prints learned clauses (first learned, first printed).
-
SimDllPrintOpen()
- Print the open propositions.
-
SimDllPrintPath()
- Print the search path.
-
SimDllPrintStack()
- Print the search stack.
-
SimDllRelsatHeur()
- Chooses the best literal according to Relsat 2.0 heuristics.
-
SimDllResolveWithWr()
- Resolves the given clause with the working reason.
-
SimDllRetractPropFF()
- Unvaluates a proposition (assigned to SIM_FF)
-
SimDllRetractPropTT()
- Unvaluates a proposition (assigned to SIM_TT)
-
SimDllRndHeur()
- Selects an open literal randomly
-
SimDllSatoHeur()
- Choose the best literal according to Sato 3.2 heuristics.
-
SimDllSatzHeur()
- Choose the best literal according to Satz heuristics.
-
SimDllSetMemout()
- Sets the memeout on the process.
-
SimDllSetTimeout()
- Sets the timeout on the process.
-
SimDllStartMemory()
- Starts memory accounting.
-
SimDllStartTimer()
- Starts a timer.
-
SimDllStopMemory()
- Stops memory accounting.
-
SimDllStopTimer()
- Stops a timer.
-
SimDllThrow()
- Prompts an error to the user and raises a SIGUSR1.
-
SimDllTraceLeafs()
- Tracing search leafs.
-
SimDllTraceNodes()
- Tracing search nodes.
-
SimDllUnitieHeur()
- A simple unit based heuristics with tie breaking.
-
SimDllUnlearnClause()
- Delete clause from learned clauses database.
-
SimDllUsrHeur()
- Asks the user for a literal.
-
SimPropClear()
- Clears a proposition.
-
SimPropInit()
- Initializes a proposition.
-
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_DllClear()
- Destroys the internal data structure.
-
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_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_DllInit()
- Initialize the DLL module. The array `params' must
be suitably initialized.
-
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_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_DllParseDimacs()
- Parses a DIMACS cnf problem file into a DLL module.
-
Sim_DllPrintFormulaDimacs()
- Print the formula in the DLL module using DIMACS format.
-
Sim_DllPrintModel()
- Print the model.
-
Sim_DllPrintParams()
- Prints parameters (configuration).
-
Sim_DllPrintResult()
- Prints the result (formatted).
-
Sim_DllPrintStats()
- Prints internal statistics.
-
Sim_DllPrintTimers()
- Prints internal timers.
-
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_DllSolve()
- Solves a formula using the Davis-Logemann-Loveland
algorithm.
-
Sim_GetErrorCode()
- Returns the error code (if any).
-
Sim_GetErrorLocation()
- Returns the error location (if any).
-
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.
-
()
- Adds a given number to a statistic.
-
()
- Assigns a truth value to a proposition and propagates it
throughout the formula doing unit resolutions only.
-
()
- Bit annotarion in proposition pointers.
-
()
- Calls the selected heuristics.
-
()
- Checks if a solution is found.
-
()
- Decides what kind of consistency check is to be performed.
-
()
- Decrements a statistic.
-
()
- Empty macro.
-
()
- Empty macro.
-
()
- Increments a statistic.
-
()
- Increments the unit counter (unit).
-
()
- Increments the unit counter (unit).
-
()
- Increments the unit counter (unit).
-
()
- Performs unit propagation.
-
()
- Prints a message about a contradiction.
-
()
- Prints a message about a skipped choice point.
-
()
- Prints a message about a split.
-
()
- Prints a message about an heuristics choice.
-
()
- Prints a message about an implied assignment.
-
()
- Prints a message about learning a clause.
-
()
- Prints a message about retracting a valuation.
-
()
- Prints a message about the creation of a new working reason.
-
()
- Prints a message about the current working reason.
-
()
- Remove a clause.
-
()
- Resets propagations.
-
()
- Return the absolute value of an integer.
-
()
- Returns a long integer in the range [0, x-1
-
()
- Selects how to propagate the proposition.
-
()
- Selects how to propagate the proposition.
-
()
- Selects the backtracking function.
-
()
- Set the flags that witness an assignment.
-
()
- Sim `assert' macro.
-
()
- Sim memory checking macro.
-
()
- Sim trace enabler.
-
()
- Store q reason.
-
()
- Stores the random generation seed.
-
()
- Swaps two scalars.
-
()
- Tests if the clause is open.
-
()
- 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.
-
()
- Updates a (maximum) statistic.
-
()
- Updates a (minimum) statistic.
-
()
- When to call MLF.
Last updated on 2009/03/04 13h:34