Documentation

Solver
in package

Tags
author

Nils Adermann naderman@naderman.de

Table of Contents

BRANCH_LEVEL  = 1
BRANCH_LITERALS  = 0
$testFlagLearnedPositiveLiteral  : bool
$branches  : array<string|int, array<string|int, mixed>>
$decisions  : Decisions
$installed  : RepositoryInterface
$installedMap  : array<string|int, int>
$io  : IOInterface
$jobs  : array<string|int, mixed>
$learnedPool  : array<string|int, mixed>
$learnedWhy  : array<string|int, mixed>
$policy  : PolicyInterface
$pool  : Pool
$problems  : array<string|int, Problem>
$propagateIndex  : int
$rules  : RuleSet
$ruleSetGenerator  : RuleSetGenerator
$updateMap  : array<string|int, int>
$watchGraph  : RuleWatchGraph
__construct()  : mixed
getRuleSetSize()  : int
solve()  : array<string|int, mixed>
analyze()  : array<string|int, mixed>
checkForRootRequireProblems()  : mixed
propagate()  : Rule|null
Makes a decision and propagates it to all rules.
setupInstalledMap()  : mixed
analyzeUnsolvable()  : int
analyzeUnsolvableRule()  : mixed
disableProblem()  : mixed
enableDisableLearnedRules()  : mixed
enable/disable learnt rules
makeAssertionRuleDecisions()  : mixed
resetSolver()  : mixed
revert()  : mixed
Reverts a decision at the given level.
runSat()  : mixed
selectAndInstall()  : int
setPropagateLearn()  : int
setpropagatelearn

Constants

BRANCH_LEVEL

public mixed BRANCH_LEVEL = 1

BRANCH_LITERALS

public mixed BRANCH_LITERALS = 0

Properties

$testFlagLearnedPositiveLiteral

public bool $testFlagLearnedPositiveLiteral = false

$branches

protected array<string|int, array<string|int, mixed>> $branches = array()

$installedMap

protected array<string|int, int> $installedMap

$jobs

protected array<string|int, mixed> $jobs

$learnedPool

protected array<string|int, mixed> $learnedPool = array()

$learnedWhy

protected array<string|int, mixed> $learnedWhy = array()

$propagateIndex

protected int $propagateIndex

$updateMap

protected array<string|int, int> $updateMap = array()

Methods

getRuleSetSize()

public getRuleSetSize() : int
Return values
int —

solve()

public solve(Request $request[, bool $ignorePlatformReqs = false ]) : array<string|int, mixed>
Parameters
$request : Request
$ignorePlatformReqs : bool = false
Return values
array<string|int, mixed> —

analyze()

protected analyze(int $level, Rule $rule) : array<string|int, mixed>
Parameters
$level : int
$rule : Rule
Return values
array<string|int, mixed> —

checkForRootRequireProblems()

protected checkForRootRequireProblems(bool $ignorePlatformReqs) : mixed
Parameters
$ignorePlatformReqs : bool
Return values
mixed —

propagate()

Makes a decision and propagates it to all rules.

protected propagate(int $level) : Rule|null

Evaluates each term affected by the decision (linked through watches) If we find unit rules we make new decisions based on them

Parameters
$level : int
Return values
Rule|null —

A rule on conflict, otherwise null.

setupInstalledMap()

protected setupInstalledMap() : mixed
Return values
mixed —

analyzeUnsolvable()

private analyzeUnsolvable(Rule $conflictRule, bool $disableRules) : int
Parameters
$conflictRule : Rule
$disableRules : bool
Return values
int —

analyzeUnsolvableRule()

private analyzeUnsolvableRule(Problem $problem, Rule $conflictRule) : mixed
Parameters
$problem : Problem
$conflictRule : Rule
Return values
mixed —

disableProblem()

private disableProblem(Rule $why) : mixed
Parameters
$why : Rule
Return values
mixed —

enableDisableLearnedRules()

enable/disable learnt rules

private enableDisableLearnedRules() : mixed

we have enabled or disabled some of our rules. We now re-enable all of our learnt rules except the ones that were learnt from rules that are now disabled.

Return values
mixed —

makeAssertionRuleDecisions()

private makeAssertionRuleDecisions() : mixed
Return values
mixed —

resetSolver()

private resetSolver() : mixed
Return values
mixed —

revert()

Reverts a decision at the given level.

private revert(int $level) : mixed
Parameters
$level : int
Return values
mixed —

runSat()

private runSat([bool $disableRules = true ]) : mixed
Parameters
$disableRules : bool = true
Return values
mixed —

selectAndInstall()

private selectAndInstall(int $level, array<string|int, mixed> $decisionQueue, bool $disableRules, Rule $rule) : int
Parameters
$level : int
$decisionQueue : array<string|int, mixed>
$disableRules : bool
$rule : Rule
Return values
int —

setPropagateLearn()

setpropagatelearn

private setPropagateLearn(int $level, string|int $literal, bool $disableRules, Rule $rule) : int

add free decision (a positive literal) to decision queue increase level and propagate decision return if no conflict.

in conflict case, analyze conflict rule, add resulting rule to learnt rule set, make decision from learnt rule (always unit) and re-propagate.

returns the new solver level or 0 if unsolvable

Parameters
$level : int
$literal : string|int
$disableRules : bool
$rule : Rule
Return values
int —

Search results