From 66cc2cc3b2f24d403167fd4e35cd69011d334b00 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sun, 10 May 2020 18:38:20 +0200 Subject: measurement time statistics + activation selection strategies --- .../reasoner/dse/ActivationSelector.xtend | 24 +++++++++ .../reasoner/dse/BalancedActivationSelector.xtend | 51 ++++++++++++++++++ .../dse/BestFirstStrategyForModelGeneration.java | 9 ++-- .../reasoner/dse/EvenActivationSelector.xtend | 20 +++++++ .../dse/ModelGenerationCompositeObjective.xtend | 12 +++-- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 63 +++++++++++++++++++--- 6 files changed, 161 insertions(+), 18 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend new file mode 100644 index 00000000..65f9814c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend @@ -0,0 +1,24 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.ArrayList +import java.util.Collection +import java.util.Random + +abstract class ActivationSelector { + long runtime = 0 + protected val Random r + new(Random r) { + this.r = r + } + + def randomizeActivationIDs(Collection activationIDs) { + val startTime = System.nanoTime + val res = internalRandomizationOfActivationIDs(activationIDs) + runtime+= System.nanoTime-startTime + return res + } + def protected ArrayList internalRandomizationOfActivationIDs(Collection activationIDs); + def getRuntime(){ + return runtime + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend new file mode 100644 index 00000000..2df9957b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend @@ -0,0 +1,51 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.Collection +import java.util.HashMap +import java.util.Map +import java.util.List +import java.util.Random +import java.util.ArrayList +import java.util.LinkedList +import java.util.Collections + +class BalancedActivationSelector extends ActivationSelector{ + val Random r = new Random + + new(Random r) { + super(r) + } + + override protected internalRandomizationOfActivationIDs(Collection activationIDs) { + val Map> urns = new HashMap + val res = new ArrayList(activationIDs.size) + for(activationID : activationIDs) { + val pair = activationID as Pair + val name = pair.key + val selectedUrn = urns.get(name) + if(selectedUrn!==null) { + selectedUrn.add(activationID) + } else { + val collection = new LinkedList + collection.add(activationID) + urns.put(name,collection) + } + } + + for(list:urns.values) { + Collections.shuffle(list,r) + } + + while(!urns.empty) { + val randomEntry = urns.entrySet.get(r.nextInt(urns.size)) + val list = randomEntry.value + val removedLast = list.remove(list.size-1) + res.add(removedLast) + if(list.empty) { + urns.remove(randomEntry.key) + } + } + return res + } + +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index 1cd61e9a..18fe94e4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -84,13 +84,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private ModelResult modelResultByInternalSolver = null; private Random random = new Random(); //private Collection> matchers; - + public ActivationSelector activationSelector = new EvenActivationSelector(random); + public NumericSolver numericSolver = null; // Statistics private int numberOfStatecoderFail = 0; private int numberOfPrintedModel = 0; private int numberOfSolverCalls = 0; - private NumericSolver numericSolver = null; public BestFirstStrategyForModelGeneration( ReasonerWorkspace workspace, @@ -137,7 +137,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { } }; - this.numericSolver = new NumericSolver(context, method); + this.numericSolver = new NumericSolver(context, method, false); trajectoiresToExplore = new PriorityQueue(11, comparator); } @@ -273,8 +273,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private List selectActivation() { List activationIds; try { - activationIds = new ArrayList(context.getUntraversedActivationIds()); - Collections.shuffle(activationIds); + activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds()); } catch (NullPointerException e) { numberOfStatecoderFail++; activationIds = Collections.emptyList(); diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend new file mode 100644 index 00000000..82a5f32d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend @@ -0,0 +1,20 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import java.util.Random +import java.util.Collection +import java.util.Collections +import java.util.ArrayList + +class EvenActivationSelector extends ActivationSelector { + + new(Random r) { + super(r) + } + + override protected internalRandomizationOfActivationIDs(Collection activationIDs) { + val toShuffle = new ArrayList(activationIDs); + Collections.shuffle(toShuffle); + return toShuffle + } + +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index 2489c751..a75ddf76 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -50,20 +50,22 @@ class ModelGenerationCompositeObjective implements IObjective{ override getComparator() { Comparators.LOWER_IS_BETTER } override getFitness(ThreadContext context) { - var sum = 0.0 + val scopeFitnes = scopeObjective.getFitness(context) //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) - sum+=scopeFitnes + var multiplicity = 0.0 for(multiplicityObjective : unfinishedMultiplicityObjectives) { - multiplicity+=multiplicityObjective.getFitness(context)//*0.5 + multiplicity+=multiplicityObjective.getFitness(context) } - sum+=multiplicity + var sum = 0.0 + sum += scopeFitnes + sum +=Math.sqrt(multiplicity *0.1) sum += unfinishedWFsFitness//*0.5 - //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') + println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') return sum } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index e1745854..71793aa6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -19,13 +19,23 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import java.util.List import java.math.BigDecimal +import java.util.LinkedHashSet +import java.util.LinkedHashMap class NumericSolver { val ThreadContext threadContext; val constraint2UnitPropagationPrecondition = new HashMap> NumericTranslator t = new NumericTranslator - new(ThreadContext threadContext, ModelGenerationMethod method) { + val boolean caching; + Map>>,Boolean> satisfiabilityCache = new HashMap + + var long runtime = 0 + var long cachingTime = 0 + var int numberOfSolverCalls = 0 + var int numberOfCachedSolverCalls = 0 + + new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { this.threadContext = threadContext val engine = threadContext.queryEngine for(entry : method.unitPropagationPreconditions.entrySet) { @@ -34,11 +44,20 @@ class NumericSolver { val matcher = querySpec.getMatcher(engine); constraint2UnitPropagationPrecondition.put(constraint,matcher) } + this.caching = caching } + def getRuntime(){runtime} + def getCachingTime(){cachingTime} + def getNumberOfSolverCalls(){numberOfSolverCalls} + def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} + def boolean isSatisfiable() { - if(constraint2UnitPropagationPrecondition.empty) return true - else { + val start = System.nanoTime + var boolean finalResult + if(constraint2UnitPropagationPrecondition.empty){ + finalResult=true + } else { val propagatedConstraints = new HashMap for(entry : constraint2UnitPropagationPrecondition.entrySet) { val constraint = entry.key @@ -47,15 +66,43 @@ class NumericSolver { //println(allMatches.toList) propagatedConstraints.put(constraint,allMatches) } - if(propagatedConstraints.values.forall[empty]) { - return true + finalResult=true } else { - val res = t.delegateIsSatisfiable(propagatedConstraints) - //println(res) - return res + if(caching) { + val code = getCode(propagatedConstraints) + val cachedResult = satisfiabilityCache.get(code) + if(cachedResult === null) { + // println('''new problem, call solver''') + // for(entry : code.entrySet) { + // println('''«entry.key» -> «entry.value»''') + // } + //println(code.hashCode) + this.numberOfSolverCalls++ + val res = t.delegateIsSatisfiable(propagatedConstraints) + satisfiabilityCache.put(code,res) + finalResult=res + } else { + //println('''similar problem, answer from cache''') + finalResult=cachedResult + this.numberOfCachedSolverCalls++ + } + } else { + finalResult= t.delegateIsSatisfiable(propagatedConstraints) + this.numberOfSolverCalls++ + } } } + this.runtime+=System.nanoTime-start + return finalResult + } + + def getCode(HashMap> propagatedConstraints) { + val start = System.nanoTime + val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList + val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) + this.cachingTime += System.nanoTime-start + return res } def fillSolutionCopy(Map trace) { -- cgit v1.2.3-54-g00ecf