From f06427cd7375551582461f91b3458339a8227f9b Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 2 Nov 2020 02:02:40 +0100 Subject: Optimizing generator with linear objective functions --- .../reasoner/dse/ViatraReasonerSolutionSaver.xtend | 112 +++++++++++++++++++-- 1 file changed, 105 insertions(+), 7 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend index c0b5008c..e00f76ff 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend @@ -1,5 +1,9 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold import java.util.HashMap import java.util.Map import org.eclipse.viatra.dse.api.DSEException @@ -18,24 +22,32 @@ import org.eclipse.xtend.lib.annotations.Accessors * Will also automatically fill any missing numerical values in the saved solutions * using the supplied {@link NumericSolver}. */ -class ViatraReasonerSolutionSaver implements ISolutionSaver { +class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider { + static val TOLERANCE = 1e-10 + @Accessors val SolutionCopier solutionCopier - val NumericSolver numericSolver @Accessors val DiversityChecker diversityChecker + val IObjective[][] leveledExtremalObjectives val boolean hasExtremalObjectives val int numberOfRequiredSolutions val ObjectiveComparatorHelper comparatorHelper val Map trajectories = new HashMap - @Accessors(PUBLIC_SETTER) var Map solutionsCollection + @Accessors var NumericSolver numericSolver + @Accessors var Map solutionsCollection - new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) { + new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { this.diversityChecker = diversityChecker comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) + this.leveledExtremalObjectives = leveledExtremalObjectives hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] this.numberOfRequiredSolutions = numberOfRequiredSolutions - this.solutionCopier = new SolutionCopier(numericSolver) + this.solutionCopier = new SolutionCopier + } + + def setNumericSolver(NumericSolver numericSolver) { this.numericSolver = numericSolver + solutionCopier.numericSolver = numericSolver } override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { @@ -51,6 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { if (!shouldSaveSolution(fitness, context)) { return false } + println("Found: " + fitness) val dominatedTrajectories = newArrayList for (entry : trajectories.entrySet) { val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) @@ -99,7 +112,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { } private def shouldSaveSolution(Fitness fitness, ThreadContext context) { - return fitness.satisifiesHardObjectives && numericSolver.currentSatisfiable + fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable) } private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, @@ -145,8 +158,93 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { } solutionsCollection.size < numberOfRequiredSolutions } - + def getTotalCopierRuntime() { solutionCopier.totalCopierRuntime } + + override computeRequiredBounds(IObjective objective, Bounds bounds) { + if (!hasExtremalObjectives) { + return + } + if (objective instanceof DirectionalThresholdObjective) { + switch (threshold : objective.threshold) { + case ObjectiveThreshold.NO_THRESHOLD: { + // No threshold to set. + } + ObjectiveThreshold.Exclusive: { + switch (kind : objective.kind) { + case HIGHER_IS_BETTER: + bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int) + case LOWER_IS_BETTER: + bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int) + default: + throw new IllegalArgumentException("Unknown objective kind" + kind) + } + if (threshold.clampToThreshold) { + return + } + } + ObjectiveThreshold.Inclusive: { + switch (kind : objective.kind) { + case HIGHER_IS_BETTER: + bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int) + case LOWER_IS_BETTER: + bounds.tightenUpperBound(Math.floor(threshold.threshold) as int) + default: + throw new IllegalArgumentException("Unknown objective kind" + kind) + } + if (threshold.clampToThreshold) { + return + } + } + default: + throw new IllegalArgumentException("Unknown threshold: " + threshold) + } + for (level : leveledExtremalObjectives) { + switch (level.size) { + case 0: { + // Nothing to do, wait for the next level. + } + case 1: { + val primaryObjective = level.get(0) + if (primaryObjective != objective) { + // There are no worst-case bounds for secondary objectives. + return + } + } + default: + // There are no worst-case bounds for Pareto front calculation. + return + } + } + val fitnessIterator = trajectories.values.iterator + if (!fitnessIterator.hasNext) { + return + } + val fitness = fitnessIterator.next.get(objective.name) + while (fitnessIterator.hasNext) { + val otherFitness = fitnessIterator.next.get(objective.name) + if (Math.abs(fitness - otherFitness) > TOLERANCE) { + throw new IllegalStateException("Inconsistent fitness: " + objective.name) + } + } + switch (kind : objective.kind) { + case HIGHER_IS_BETTER: + if (needsMoreSolutionsWithSameFitness) { + bounds.tightenLowerBound(Math.floor(fitness) as int) + } else { + bounds.tightenLowerBound(Math.floor(fitness + 1) as int) + } + case LOWER_IS_BETTER: + if (needsMoreSolutionsWithSameFitness) { + bounds.tightenUpperBound(Math.ceil(fitness) as int) + } else { + bounds.tightenUpperBound(Math.ceil(fitness - 1) as int) + } + default: + throw new IllegalArgumentException("Unknown objective kind" + kind) + } + } + } } -- cgit v1.2.3-54-g00ecf