Internal functions and data strucures of the SIM package.

static int 
CountBinaryNeg(
  SimProp_t * p 
)
Evaluates how many times a propositions occurres in a binary clause. If PURE LITERAL is defined returns the number of occurrences in clauses of any length.

Side Effects none

See Also SimDllRelsatHeur
Defined in simHeur.c

static int 
CountBinaryPos(
  SimProp_t * p 
)
Evaluates how many times a propositions occurres in a binary clause. If PURE LITERAL is defined returns the number of occurrences in clauses of any length.

Side Effects none

See Also SimDllRelsatHeur
Defined in simHeur.c

static int 
CountNoBinaryNeg(
  SimProp_t * p 
)
Uses a modified JW weighting function H(x): for each open proposition x compute the sum H(x) of the quantities 2^(2^(JW_MAX - |C|)) (which defaults to 1 if |C| >= JW_MAX) for each clause C where l occurs.

Side Effects none

See Also SimDllRelsatHeur
Defined in simHeur.c

static int 
CountNoBinaryPos(
  SimProp_t * p 
)
Uses a modified JW weighting function H(x): for each open proposition x compute the sum H(x) of the quantities 2^(2^(JW_MAX - |C|)) (which defaults to 1 if |C| >= JW_MAX) for each clause C where l occurs.

Side Effects none

See Also SimDllRelsatHeur
Defined in simHeur.c

static SimProp_t * 
DllMomsHeur(
  int * sign, 
  int * mode, 
  SimProp_t ** propList, 
  int  signPos 
)
For each open proposition x computes the score f(x) * f(-x), where f is the number of occurrence in binary clauses. Chooses the proposition with the highest score. The sign is `signPos' if f(x) > f(-x), and -`signPos' otherwise. If `propList' (a list of positive integers) is non-0, the heuristics looks at the contents of `propList' instead of looking at the open propositions (in the spirit of SATO 3.2).

Side Effects None

See Also SimDllSatoHeur
Defined in simHeur.c

static int 
Examine0(
  SimProp_t * p, 
  int  sign, 
  int * reduced 
)
Assigns the proposition p with a certain sign and then performs unit propagation, collecting scores; at the end all the changes are undone. Returns SIM_UNSAT if p is a failed literal and SIM_SAT otherwise.

See Also SimDllSatzHeur Examine ExtendProp Bcp ResetProps
Defined in simHeur.c

static int 
Examine(
  SimProp_t * p, 
  int  sign, 
  int * reduced 
)
Assigns the proposition p with a certain sign and then performs unit propagation collecting, scores; at the end all the changes are undone. Returns SIM_UNSAT if p is a failed literal and SIM_SAT otherwise.

Side Effects None

See Also SimDllSatzHeur Examine0 ExtendProp Bcp ResetProps
Defined in simHeur.c

static int 
Propagate(
  SimProp_t * p, 
  int  sign, 
  int * score 
)
Assigns the proposition p with a certain sign and then performs unit propagation collecting scores; at the end all the changes are undone. Returns SIM_UNSAT if p is a failed literal and SIM_SAT otherwise.

Side Effects None

See Also SimDllRelsatHeur
Defined in simHeur.c

void 
SimClauseClear(
  SimClause_t * cl 
)
Clears a clause.

Side Effects none

Defined in simClause.c

SimClause_t* 
SimClauseInit(
  int  clId, 
  size_t  clSize 
)
Initializes a clause.

Side Effects none

Defined in simClause.c

SimProp_t * 
SimDll2JWHeur(
  int * sign, 
  int * mode 
)
Assign weight to propositions according to the 2 sided Jeroslow and Wang heuristics: JW(x) + JX(-x). Suggest positive sign if JW(x) >= JW(-x), negative sign otherwise. Break ties using a position argument: the first proposition that scores highest is the best. (From "Branching Rules for Satisfiability, by J. N. Hooker and V. Vinay, Journal of Automated Reasoning 15(3), 1995").

Side Effects none

See Also Sim_DllSolve
Defined in simHeur.c

SimProp_t * 
SimDllBackjumping(
  int * sign, 
  int * mode 
)
Backtracks to the most recent open choice point that was responsible for the contradiction, possibly skipping other choice points. If LEARNING is defined, also stores working reasons with some criterion and propagates unit learned clauses. Returns a reference to the proposition at the choice point or 0 when there is no more choice, i.e., an attempt to backtrack beyond the very first choice point is made.

Side Effects none

See Also Sim_DllSolve SimDllRetractProp
Defined in simLookBack.c

int 
SimDllBcp(
    
)
Keeps propagating unit clauses until an empty clause is found or no more unit clauses are created. If BACKJUMPING is definded stores the reason of the unit propagation. If LEARNING is defined discards subsumed clauses. Returns SIM_UNSAT if an empty clause is found, SIM_SAT otherwise.

Side Effects none

See Also Sim_DllSolve SimDllExtendProp
Defined in simLookAhead.c

SimProp_t * 
SimDllBoehmHeur(
  int * sign, 
  int * mode 
)
Select the proposition with the biggest weight vector in lexicopgraphic order. For each proposition x the weight vector is (H(x),H'(x)), where and h(x) is the number of occurrences of x in the shortest clauses, while h'(x) is the number of occurrences in all the clauses. From "Report on a SAT competition, by M.Buro and H. Kleine Buning, Bericht Nr. 110, Reihe Informatik, November 1992", in the spirit of Boehm's solver version A 31/3/92.

Side Effects None

See Also Sim_DllSolve
Defined in simHeur.c

void 
SimDllBuild(
    
)
Completes the initialization of the internal data structure before the search begins.

Side Effects none

See Also Sim_DllInit Sim_DllClear
Defined in simData.c

int 
SimDllCheck(
  int * redundant 
)
Reinitializes the number of open literals in each clause and then propagates the stack contents throughout the formula (from stack bottom to stack top) using a simple algorithm. Returns SIM_UNSAT if: and SIM_SAT otherwise. If HORN_RELAXATION is defined checks the number of open non-Horn clauses. If LEARNING is defined checks also resolutions on learned clauses.

Side Effects redundant is set to the number of unnecessary assignments.

Defined in simSolve.c

SimProp_t * 
SimDllChronoBt(
  int * sign, 
  int * mode 
)
Backtracks to the most recent open choice point, i.e., the most recent proposition assigned with SIMLSPLIT mode. Returns a reference to the proposition at the choice point or NULL when there is no more choice, i.e., an attempt to backtrack beyond the very first choice point is made.

Side Effects none

See Also Sim_DllSolve SimDllRetractProp
Defined in simLookBack.c

void 
SimDllDelProp(
  SimProp_t * p 
)
Removes a literal from the DLL data structure.

Side Effects none

See Also Sim_DllAddClause
Defined in simData.c

void 
SimDllEndRelsatHeur(
    
)
Free auxiliary data for Relsat heuristics.

Side Effects None

See Also SimDllInitRelsatHeur SimDllRelsatHeur
Defined in simHeur.c

void 
SimDllEndSatoHeur(
    
)
Free auxiliary data for Sato heuristics.

Side Effects none

See Also SimDllInitSatoHeur SimDllSatoHeur
Defined in simHeur.c

void 
SimDllEndSatzHeur(
    
)
Free auxiliary data for Chu Min Li heuristics.

Side Effects None

See Also SimDllInitSatzHeur SimDllSatzHeur
Defined in simHeur.c

void 
SimDllEndUnitieHeur(
    
)
Free auxiliary data for Unitie heuristics.

Side Effects None

See Also SimDllInitUnitieHeur SimDllUnitieHeur
Defined in simHeur.c

int 
SimDllExtendPropFF(
  SimProp_t * p, 
  int  mode 
)
Considers a proposition and its valuation: propagates the valuation through the formula. Unit clauses are detected and pushed onto the Bcp stack. If HORN_RELAXATION is enabled, the non-Horn to Horn transitions are monitored and the non horn index is suitably updated. If BACKJUMPING is defined, stores the empty clauses causeed by conflicts. If LEARNING is defined, the valuation is propagated to the learned clauses (unit resolutions only). Returns SIM_UNSAT if an empty clause is found; SIM_SAT otherwise.

Side Effects none

See Also SimDllRetractProp SimDllBcp SimDllMlf
Defined in simSolve.c

int 
SimDllExtendPropTT(
  SimProp_t * p, 
  int  mode 
)
Considers a proposition and its valuation: propagates the valuation through the formula. Unit clauses are detected and pushed onto the Bcp stack. If HORN_RELAXATION is enabled, the non-Horn to Horn transitions are monitored and the non horn index is suitably updated. If BACKJUMPING is defined, stores the empty clauses causeed by conflicts. If LEARNING is defined, the valuation is propagated to the learned clauses (unit resolutions only). Returns SIM_UNSAT if an empty clause is found; SIM_SAT otherwise.

Side Effects none

See Also SimDllRetractProp SimDllBcp SimDllMlf
Defined in simSolve.c

int 
SimDllGetModelsHorn(
  int * stop 
)
Consistency checking with horn relaxation.

Side Effects none

See Also Sim_DllSolve
Defined in simCons.c

int 
SimDllGetModels(
  int * stop 
)
Consistency checking.

Side Effects none

See Also Sim_DllSolve
Defined in simCons.c

void 
SimDllInitRelsatHeur(
    
)
Allocate auxiliary data for Relsat heuristics.

Side Effects none

See Also SimDllRelsatHeur SimDllEndRelsatHeur
Defined in simHeur.c

void 
SimDllInitSatoHeur(
    
)
Allocate auxiliary data for Sato 3.2 heuristics.

Side Effects none

See Also SimDllSatoHeur SimDllEndSatoHeur
Defined in simHeur.c

void 
SimDllInitSatzHeur(
    
)
Allocate auxiliary data for Chu Min Li heuristics.

Side Effects None

See Also SimDllSatzHeur SimDllEndSatzHeur
Defined in simHeur.c

void 
SimDllInitUnitieHeur(
    
)
Allocate auxiliary data for Uniti heuristics.

Side Effects None

See Also SimDllUnitieHeur SimDllEndUnitieHeur
Defined in simHeur.c

void 
SimDllInitWr(
  SimClause_t * cl 
)
Cleans the flags to test membership in the working reason and stores the literals of the conflict (empty) clause.

Side Effects none

See Also SimDllBackjumping
Defined in simLookBack.c

SimProp_t * 
SimDllInsProp(
  int  lit, 
  SimClause_t * cl 
)
Inserts a new proposition in the DLL data structure.

Side Effects none

See Also Sim_DllAddClause
Defined in simData.c

SimProp_t * 
SimDllJWHeur(
  int * sign, 
  int * mode 
)
For each open literal l compute the sum J(l) of the quantities 2^(JW_MAX - |C|) (which defaults to 1 if |C| > JW_MAX) for each clause C where l occurs. Branch to the literal l having the highest weight J(l). Break ties using a position argument: the first literal that scores highest is the best (From "Branching Rules for Satisfiability, by J. N. Hooker and V. Vinay, Journal of Automated Reasoning 15(3), 1995").

Side Effects None

See Also Sim_DllSolve
Defined in simHeur.c

void 
SimDllLearnClause(
  SimClause_t * cl 
)
Adds the clause to the list of learned clauses and links the occurrences of propositions in the clause.

See Also SimDllBackjumping
Defined in simLookBack.c

SimClause_t * 
SimDllMakeClauseFromWr(
  int  optimize 
)
Creates a clause from the working reason.

Side Effects none

See Also SimDllBackjumping
Defined in simLookBack.c

void 
SimDllMlf(
    
)
Propagates all the pure literals in the MLF stack. If the literal was propagate with another mode it is discarded.

Side Effects none

See Also Sim_DllSolve SimDllExtendProp
Defined in simLookAhead.c

SimProp_t * 
SimDllMomsHeur(
  int * sign, 
  int * mode 
)
An interface to DllMomsHeur.

Side Effects None

See Also SimDllSatoHeur
Defined in simHeur.c

void 
SimDllParseDimacsCls(
  FILE * inFile 
)
Takes a reference to a file and tries to parse non tautolougus *sets* of literals (clauses). Duplicate literals are removed. Tautologies and empty clauses are discarded. The parsing is successfull only when the clause does not fall in the above categories. This function does not sort the literals in the clauses.

Side Effects none

See Also Sim_DllParseDimacsFile
Defined in simParse.c

void 
SimDllPrintClause(
  SimClause_t * cl 
)
Prints a clause structure.

Side Effects None

See Also Sim_DllUsrHeur
Defined in simOutput.c

void 
SimDllPrintFormulaStruct(
    
)
Print the formula in the DLL module using a special format: Also the following internal state information is printed in a trailer:

Side Effects None

See Also Sim_DllPrintFormulaDimacs
Defined in simOutput.c

void 
SimDllPrintLearnedBW(
  int  n 
)
Prints learned clauses (last learned, first printed). if n is less than the number of learned clauses, prints n clauses from the bottom.

Side Effects None

Defined in simOutput.c

void 
SimDllPrintLearnedFW(
  int  n 
)
Prints learned clauses (first learned, first printed). If n is less than the number of learned clauses prints n learned clauses from the top.

Side Effects None

Defined in simOutput.c

void 
SimDllPrintOpen(
    
)
Print the open propositions.

Side Effects None

See Also SimDllUsrHeur
Defined in simOutput.c

void 
SimDllPrintPath(
    
)
Print the search path.

Side Effects None

See Also Sim_DllPrintModel
Defined in simOutput.c

void 
SimDllPrintStack(
    
)
Print the search stack.

Side Effects None

See Also Sim_DllPrintModel
Defined in simOutput.c

SimProp_t * 
SimDllRelsatHeur(
  int * sign, 
  int * mode 
)
Scores the open propositions according to the number of their binary occurrences. If a proposition fullfills some additional requirements then it is propagated and failed assignments are detected. If no failed literal is detected, a pool of variables that scores in within RELSAT_FUDGEFACT of the best weight is collected. A variable and a sign are then chosen randomly. (In the spirit of Relsat 2.0 code)

Side Effects none

See Also Sim_DllSolve
Defined in simHeur.c

void 
SimDllResolveWithWr(
  SimClause_t * cl, 
  SimProp_t * pRes 
)
Resolves the given clause with the working reason.

Side Effects none

See Also SimDllBackjumping
Defined in simLookBack.c

void 
SimDllRetractPropFF(
  SimProp_t * p 
)
Considers a proposition: the effects of the propagations are undone through the formula. Unit clauses are detected and pushed onto the Bcp stack. If HORN_RELAXATION is enabled, the non-horn to horn transitions are monitored and the non-horn index is suitably restored. If BACKJUMPING is enabled, removes the reason of failure driven assignments. If LEARNING is defined, updates learned clauses, and detects unit on learned clauses.

Side Effects none

See Also SimDllRetractProp SimDllBcp SimDllMlf
Defined in simSolve.c

void 
SimDllRetractPropTT(
  SimProp_t * p 
)
Considers a proposition: the effects of the propagations are undone through the formula. Unit clauses are detected and pushed onto the Bcp stack. If HORN_RELAXATION is enabled, the non-horn to horn transitions are monitored and the non-horn index is suitably restored. If BACKJUMPING is enabled, removes the reason of failure driven assignments. If LEARNING is defined, updates learned clauses, and detects unit on learned clauses.

Side Effects none

See Also SimDllRetractProp SimDllBcp SimDllMlf
Defined in simSolve.c

SimProp_t * 
SimDllRndHeur(
  int * sign, 
  int * mode 
)
Draws a number r from 0 to the number of current variables, i.e., open propositions. Then chooses the r-th open proposition with a random sign.

Side Effects none

See Also Sim_DllSolve
Defined in simHeur.c

SimProp_t * 
SimDllSatoHeur(
  int * sign, 
  int * mode 
)
If the percentage of non-Horn clauses is less than certain rate: get the propositions that occur in the shortest non-horn clauses, and select the best literal according to MOMS heuristics. Select SATO_MAGIC open non-Horn clauses and SATO_MAGIC open propositions at most. If the percentage of non-Horn clauses is bigger than the above rate or if there are less than two non-Horn clauses use MOMS heuristics only. (From "SATO: an Efficient Propostional Prover, by Hantao Zhang, proceedings of CADE, 1996" and in the spirit of SATO version 3.2).

Side Effects none

See Also Sim_DllSolve MomsHeur SimDllInitSatoHeur SimDllEndSatoHeur
Defined in simHeur.c

SimProp_t * 
SimDllSatzHeur(
  int * sign, 
  int * mode 
)
Compute the number of positive and negative occurrences for each open proposition. Then select all the propositions that have at least 4 binary occurrences, of which at least 1 positive and 1 negative (PROP41). If there are less than T propositions that satisfy this condition, then select also the propositions that have at least 3 occurrences in binary clauses, of which at least 1 positive and 1 negative (PROP31). If less than T propositions are collected, reset what has been done so far and compute weights for each open variable using BCP and a modified Jeroslow-Wang weighting function. (From "Heuristics Based on Unit Propagation for Satisfiability Problems, by Chu Min Li and Anbulagan, proceedings of AAAI, 1999" and in the spirit of SATZ, release September 1996).

Side Effects None

See Also Sim_DllSolve SimDllInitSatzHeur SimDllEndSatzHeur Examine Examine0
Defined in simHeur.c

void 
SimDllSetMemout(
  int  mmout 
)
Sets the specified memeout using the CPU resource limit mechanism.

Side Effects none

Defined in simMemory.c

void 
SimDllSetTimeout(
  int  tmout 
)
Sets the specified timeout using the CPU resource limit mechanism.

Side Effects none

Defined in simTime.c

void 
SimDllStartMemory(
  int  i 
)
Sets the given counter to the current unshared data size.

Side Effects none

Defined in simMemory.c

void 
SimDllStartTimer(
  int  timer 
)
Sets the specified timer to the current CPU resource usage.

Side Effects none

Defined in simTime.c

void 
SimDllStopMemory(
  int  i 
)
Sets the given counter to the current unshared data size minus the old counter value.

Side Effects none

Defined in simMemory.c

void 
SimDllStopTimer(
  int  timer 
)
Sets the specified timer to the current CPU resource usage minus the old timer value.

Side Effects none

Defined in simTime.c

void 
SimDllThrow(
  Sim_ErrCode_c  errCode, 
  Sim_ErrLocation_c  errLoc, 
  char * message 
)
Takes an error type and the error location in the program. Prompts the user on stderr and teminates raising the user defined signal SIGUSR1.

Side Effects none

Defined in simError.c

void 
SimDllTraceLeafs(
    
)
Each time the function is called a counter is decremented. Once the number of ticks is reached, the functions outputs data on the look-back algorithms.

Side Effects none

Defined in simTrace.c

void 
SimDllTraceNodes(
    
)
Each time the function is called a counter is decremented. Once the number of ticks is reached, the functions outputs data on the look-ahead algorithms.

Side Effects none

Defined in simTrace.c

SimProp_t * 
SimDllUnitieHeur(
  int * sign, 
  int * mode 
)
Selects all the variables that maximize the score: binIfpos * binIfneg << 1 + unitIfpos + unitIfneg + 1 and breaks ties selecting the variable that subsumes the largest number of clauses.

Side Effects none

See Also Sim_DllSolve
Defined in simHeur.c

void 
SimDllUnlearnClause(
  SimClause_t * cl 
)
Delete clause from learned clauses database.

Side Effects none

See Also SimDllBackjumping
Defined in simLookBack.c

SimProp_t * 
SimDllUsrHeur(
  int * sign, 
  int * mode 
)
Displays all the open literals and asks the user to choose among them (mainly for debugging purposes).

Side Effects none

See Also Sim_DllSolve
Defined in simHeur.c

void 
SimPropClear(
  SimProp_t * p 
)
Clears a proposition.

Side Effects none

Defined in simProp.c

SimProp_t* 
SimPropInit(
  int  prop, 
  short  litSize 
)
Initializes a proposition.

Side Effects none

Defined in simProp.c

int 
Sim_DllAddLit(
  int  clId, 
  int  lit 
)
If there is no pending clause in SimClauses, or `lit' is not within reasonable bounds, exit with error condition -1. Check for tautologies and duplications using the list of occurrences for the proposition corresponding to `lit'. Return 0 on tautologies, 1 on duplications. If the literal is ok, add it to the clause and update the lists of occurrences of the corresponding proposition.

Side Effects none

See Also Sim_DllNewCl Sim_DllNewClSize
Defined in simData.c

void 
Sim_DllClear(
    
)
Destroys the internal data structure.

Side Effects none

See Also Sim_DllInit
Defined in simData.c

int 
Sim_DllCommitCl(
  int  clId 
)
If there is no pending clause in SimClauses or it has not the same `clId', return -1. If the current clause is empty, reset the state and return 0. If the pending clause is ok, it is confirmed in the main clause index: if unary, it is pushed in the bcp stack. If HORN_RELAXATION is defined, non-Horn clauses are detected and pushed in the non-Horn index.

Side Effects none

See Also Sim_DllInit
Defined in simData.c

int * 
Sim_DllGetSolution(
    
)
Allocate `result' to contain all propositions indexes; scan the main propositions index and store in `result' the value of the corresponing literals.

Side Effects none

See Also Sim_DllGetStack
Defined in simData.c

int * 
Sim_DllGetStack(
    
)
Allocate `result' to contain all the propositions; scan the stack and store in `result' the id of the literal with the sign of propagation.

Side Effects none

See Also Sim_DllGetStack
Defined in simData.c

void 
Sim_DllInit(
  int * params 
)
Perform several initializations.

Side Effects none

See Also Sim_DllClear
Defined in simData.c

int 
Sim_DllNewClSize(
  short  size 
)
If there is a pending clause in SimClauses, return -1, a failure code. Otherwise, create a new empty clause and reference it with the last available index in SimClauses. The size of the clause will be `size'. Return the clause index (to be used in future operations with the clause).

Side Effects none

See Also Sim_DllAddLit Sim_DllCommitCl
Defined in simData.c

int 
Sim_DllNewCl(
    
)
If there is a pending clause in SimClauses, return -1, a failure code. Otherwise, create a new empty one and reference it with the last available index in SimClauses. The size of the clause will be the default SIMCL_SIZE. Return the clause index (to be used in future operations with the clause).

Side Effects none

See Also Sim_DllAddLit Sim_DllCommitCl
Defined in simData.c

int 
Sim_DllParseDimacs(
  FILE * inFile, 
  int * params 
)
Takes a pointer to a file and tries to parse (using DIMACS format) a cnf problem. Takes also the initialization parameters for the dll module. Returns a pointer to a DLL module if successfull; NULL if (i) the file does not exists, or (ii) there is no line starting with p, or (iii) such line does not define a DIMACS cnf problem.

Side Effects none

See Also Sim_DllInit
Defined in simParse.c

void 
Sim_DllPrintFormulaDimacs(
    
)
Print the formula in the DLL module using DIMACS format.

Side Effects None

Defined in simOutput.c

void 
Sim_DllPrintModel(
    
)
Print the model.

Side Effects None

See Also Sim_DllPrintStack
Defined in simOutput.c

void 
Sim_DllPrintParams(
    
)
Prints parameters (configuration).

Side Effects None

See Also Sim_DllPrintModel
Defined in simOutput.c

void 
Sim_DllPrintResult(
  int  res 
)
Prints the result (formatted).

Side Effects None

See Also Sim_DllPrintModel
Defined in simOutput.c

void 
Sim_DllPrintStats(
    
)
Prints internal statistics.

Side Effects None

See Also Sim_DllPrintModel
Defined in simOutput.c

void 
Sim_DllPrintTimers(
    
)
Prints internal timers.

Side Effects None

See Also Sim_DllPrintModel
Defined in simOutput.c

void 
Sim_DllPropMakeIndep(
  int  prop 
)
If `prop' is a sensible value, then if the corresponding proposition is not there, it is created and inserted in the main proposition index. If the proposition was not declared as a model proposition, set its back reference and push it in the model propositions index.

Side Effects none

Defined in simData.c

int 
Sim_DllSolve(
    
)
A heuristic function (SimDllChooseLiteral) is used to choose a literal at each node of the search tree; SimDllCheckConsistency is used to (i) declare a formula satisfiable, and (ii) stop the search at some point; the SimDllBacktracking function is responsible for restoring to a previous choice point (if any) in the search tree when a dead end (SIM_UNSAT subproblem) is reached. Returns SIM_SAT if the formula is satisifable; SIM_UNSAT otherwise.

Side Effects none

See Also SimDllCheckConsistency SimDllChooseLiteral SimDllBacktrack
Defined in simSolve.c

Sim_ErrCode_c 
Sim_GetErrorCode(
    
)
Returns the error code (if any).

Side Effects none

Defined in simError.c

Sim_ErrLocation_c 
Sim_GetErrorLocation(
    
)
Returns the error location (if any).

Side Effects none

Defined in simError.c

int * 
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.

Side Effects none

See Also Sim_ParamSet
Defined in simData.c

int * 
Sim_ParamSet(
  int * param, 
  int  pName, 
  int  pValue 
)
Changes the value of a specific parameter.

Side Effects none

See Also Sim_ParamInit
Defined in simData.c

 
(
    
)
Adds a given number to a statistic.

Side Effects none

See Also SimDllStatDec
Defined in simInt.h

 
(
    
)
Decrements the number of open literals (openLitNum) in each clause. If the clause does not become unary, pushes its pointer into managedCls. If the clause becomes unary, pushes it in the BCP stack.

Side Effects Every times that a unit clause is found, it is pushed into Bcp stack, and localBcpIdx is incremented. If a contradiction is found, the variable localBcpIdx is set to -1, and the propagation is stopped. Otherwise, score is incremented.

See Also LeanBcp
Defined in simHeur.c

 
(
    
)
Bit annotation in proposition pointers.

Side Effects none

Defined in simInt.h

 
(
    
)
Call the selected heuristics.

Side Effects The heuristics assigns a value to s and m.

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Checks if the number of open clauses is greater than 0. If HORN_RELAXATION is defined, checks if the number of open non-Horn clauses is greater than 0.

Side Effects none

See Also SimDllMlf
Defined in simInt.h

 
(
    
)
Calls the function that checks if the formula is empty, i.e., if the number of open clauses is 0. If HORN_RELAXATION is defined, calls the function that checks if the number of open non-Horn clauses is 0.

Side Effects The function assigns a value to s

Defined in simInt.h

 
(
    
)
Decrements a statistic.

Side Effects none

See Also SimDllStatInc
Defined in simInt.h

 
(
    
)
Empty macro.

Side Effects none

See Also Examine Examine0
Defined in simHeur.c

 
(
    
)
Empty macro.

Side Effects none

See Also Examine Examine0
Defined in simHeur.c

 
(
    
)
Increments a statistic.

Side Effects none

See Also SimDllStatDec
Defined in simInt.h

 
(
    
)
Increments the unit counter (unit).

Side Effects none

See Also Propagate
Defined in simHeur.c

 
(
    
)
Increments the unit counter (unit).

Side Effects none

See Also Propagate
Defined in simHeur.c

 
(
    
)
Increments the unit counter (unit).

Side Effects none

See Also Propagate
Defined in simHeur.c

 
(
    
)
Keeps propagating the unit clauses until an empty clause is found or there are no more unit clauses. ScoringOp and BacktrackOp are in the form `void xxxOp(SimProp_t * p)' and define additional operations to be done with q.

Side Effects The function performing ExtendProp puts -1 into the index of BCP stack when an empty clause is found.

See Also LeanExtendPropTT LeanExtendPropFF
Defined in simHeur.c

 
(
    
)
Takes a proposition.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes a proposition and a level.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes a proposition, a value and a level.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes a proposition, the heuristics name and a weight.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes a proposition, a value, a level and the reason for the implied assignment (e.g., unit, pure literal, etc.).

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes parameters for SimDllPrintClause.

Side Effects none

Defined in simInt.h

 
(
    
)
Takes a proposition, a value and a level.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes a list of literals and a temporary index.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Takes a list of literals and a temporary index.

Side Effects none

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Remove a clause.

Side Effects none

Defined in simInt.h

 
(
    
)
Restores the number of open propositions to the old value in the changed clauses. Unassigns all the propositions in changedProps.

Side Effects none

Defined in simHeur.c

 
(
    
)
Return the absolute value of an integer.

Side Effects none

Defined in simInt.h

 
(
    
)
Returns a long integer in the range [0, x-1

Side Effects none

Defined in simInt.h

 
(
    
)
Calls SimDllExtendPropTT or SimDllExtendPropFF, according to the value of sign.

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Calls SimDllExtendPropTT or SimDllExtendPropFF, according to the value of sign.

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
If BACKJUMPING is defined calls Backjumping instead of Chronological backtracking.

Side Effects The function assigns a value to s and m.

See Also Sim_DllSolve
Defined in simInt.h

 
(
    
)
Set the flags that witness an assignment.

Side Effects none

See Also Propagate
Defined in simHeur.c

 
(
    
)
If the condition is not fullfilled raises the exception SIM_INTERNAL_ERROR using the library own exception handling.

Side Effects none

Defined in simInt.h

 
(
    
)
If the second argument is NULL raises the exception SIM_MEMORY_ERROR using the library own exception handling.

Side Effects none

Defined in simInt.h

 
(
    
)
Calls the function only if TRACE is defined.

Side Effects none

Defined in simInt.h

 
(
    
)
Store q reason.

Side Effects none

See Also Propagate
Defined in simHeur.c

 
(
    
)
Stores the random generation seed.

Side Effects If `x' is zero and `getpid()' is available, x is set to the return value of `getpid()'.

Defined in simInt.h

 
(
    
)
Swaps two scalars.

Side Effects none

Defined in simInt.h

 
(
    
)
Tests if the clause is open.

Side Effects none

Defined in simInt.h

 
(
    
)
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.

Side Effects none

Defined in simHeur.c

 
(
    
)
Compares the current value with the previous value and updates the information when the current value is bigger.

Side Effects none

See Also SimDllStatInc
Defined in simInt.h

 
(
    
)
Compares the current value with the previous value and updates the information when the current value is smaller.

Side Effects none

See Also SimDllStatInc
Defined in simInt.h

 
(
    
)
If PURE_LITERAL is defined calls SimDllMlf.

See Also Sim_DllSolve
Defined in simInt.h

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