kodkod.engine.ucore

Class AdaptiveRCEStrategy

java.lang.Object

kodkod.engine.ucore.AdaptiveRCEStrategy

All Implemented Interfaces:

ReductionStrategy

public final class AdaptiveRCEStrategy
extends Object
implements ReductionStrategy

Adaptive Recycling Core Extraction is a strategy for generating unsat cores that are minimal at the logic level. Specifically, let C be a core that is minimal according to this strategy, and let F(C) be the top-level logic constraints corresponding to C. Then, this strategy guarantees that there is no clause c in C such that F(C - c) is a strict subset of F(C). Furthermore, it also guarantees that for all f in F(C), F(C) - f is satisfiable. This is a stronger guarantee than that of HybridStrategy. In general, using this strategy is more expensive, timewise, than using HybridStrategy.

Unlike RCE, ARCE is parameterized with 3 values that control the amount of recycling. The first is the noRecycleRatio, which completely disables recycling if it is greater than the ratio of the size of the core passed to next(ResolutionTrace) and the number of axioms in the trace. The default value is .03; if the core makes up only 3 percent of the axioms, no recycling will happen. The remaining two parameters are the recycleLimit and the hardnessCutOff. If the hardness of the proof passed to next(ResolutionTrace) is greater than hardnessCutOff, then the number of relevant axioms, |A_r|, plus the number of recycled resolvents is no greater than |A_r|*recycleLimit. Otherwise, all valid resolvents are recycled (i.e. added to the relevant axioms). Proof hardness is the ratio of the trace size to the number of axioms in the trace. Default value for hardnessCutOff is 2.0, and default value for recycleLimit is 1.2.

This implementation of ARCE will work properly only on CNFs generated by the kodkod Translator.

Author:

Emina Torlak

Specfields:

noRecycleRatio: double

hardnessCutOff: double

recycleLimit: double

Invariants:

noRecycleRatio in [0..1]

recycleLimit >= 1

hardnessCutOff >= 1

See Also:

HybridStrategy

Constructor Summary

Constructors

Constructor and Description
AdaptiveRCEStrategy(TranslationLog log) Constructs an ARCE strategy that will use the given translation log to relate the cnf clauses back to the logic constraints from which they were generated.
AdaptiveRCEStrategy(TranslationLog log, double noRecycleRatio, double hardnessCutOff, double recycleLimit) Constructs an ARCE strategy that will use the given translation log to relate the cnf clauses back to the logic constraints from which they were generated.

Method Summary

Modifier and Type	Method and Description
IntSet	next(ResolutionTrace trace) Returns the next subtrace of the specified trace to be analyzed, given as a set of indices into the trace.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AdaptiveRCEStrategy

public AdaptiveRCEStrategy(TranslationLog log)

Constructs an ARCE strategy that will use the given translation log to relate the cnf clauses back to the logic constraints from which they were generated.

Ensures:

this.hardnessCutOff' = 2 and this.recycleLimit' = 1.2 and this.noRecycleRatio' = .03

AdaptiveRCEStrategy

public AdaptiveRCEStrategy(TranslationLog log,
                           double noRecycleRatio,
                           double hardnessCutOff,
                           double recycleLimit)

Constructs an ARCE strategy that will use the given translation log to relate the cnf clauses back to the logic constraints from which they were generated.

Ensures:

this.hardnessCutOff' = hardnessCutOff and this.recycleLimit' = recycleLimit and this.noRecycleRatio' = noRecycleRatio

Method Detail

next

public IntSet next(ResolutionTrace trace)

Returns the next subtrace of the specified trace to be analyzed, given as a set of indices into the trace. If there are no more subtraces to be analyzed (i.e. the given trace is minimal according to the minimality measure used by this strategy), returns the empty set.

Specified by:

next in interface ReductionStrategy

Requires:

 let t = this.traces[#this.traces-1], n = this.nexts[#this.nexts-1] | 
  unsat(t.elts[n].literals) => 
   (all i: n.ints | let j = #{k: n.ints | k < i} | t.elts[i].equals(trace.elts[j])) 
  else
   trace = t
 

Ensures:

 
  let next = { i: int | 0 <= i < trace.size()-1 } |
   trace.elts[next].antecedents in trace.elts[next] and 
   (some i: [0..#trace) | i !in next and no trace[i].antecedents) and  
   this.nexts' = this.nexts + #this.nexts->next and
   this.traces' = this.traces + #this.traces->trace 
 

Returns:

this.nexts'[#this.nexts-1]

See Also:

ReductionStrategy.next(kodkod.engine.satlab.ResolutionTrace)