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
- H(x) = ALPHA * max(h(x), h(-x)) +
BETA * min(h(x), h(-x))
- H'(x) = ALPHA * max(h'(x), h'(-x)) +
BETA * min(h'(x), h'(-x))
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:
- the stack contains a proposition which has SIM_DC
or SIM_NT in its teta field, or
- an empty clause is found, or
- the number of open clauses does not become
0 after the stack has been examined,
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:
- each clause sits in a single line;
- the clause is headed by the number of open literals
in angle brackets;
- if the clause was simplified then a pair of square
brackets surrounds it;
- if a literal was resolved it appears surrounded by
normal parentheses.
Also the following internal state information is
printed in a trailer:
- search stack contents
- maximum varibale index and currently open variables
- total number of clauses, currently open clauses
and, if HORN_RELAXATION is enabled, currently open
non-horn clauses.
- 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.
- the solver working parameters are set using the values
in the input array `params';
- timeout and memory out are fixed;
- counters, statistics and timers are resetted;
- the random seed is initialized;
- the main propositions index and the propositions
look-up table are initialized
(the look-up table is to accomodate up to the
biggest variable index);
- the model propositions index is initialized to a
fraction (25%) of the number of propositions;
- if PURE_LITERAL is defined, the pure literal stack
is initialized to the number of propositions;
- the main clause index and the unit clauses stack
are initialized to the number of clauses;
- if HORN_RELAXATION is defined, the non-Horn
clauses index is initialized to the number of clauses.
- 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