Class DHitSatInconsistencyMeasure

  • All Implemented Interfaces:
    PostulateEvaluatable<PlFormula>, InconsistencyMeasure<BeliefSet<PlFormula,​?>>

    public class DHitSatInconsistencyMeasure
    extends SatBasedInconsistencyMeasure
    This class presents a sat-encoding-based implementation of the hit-distance measure of [Grant and Hunter, “Analysing inconsistent information using distance-based measures” Int. J. Approx. Reasoning, 2017]. The hit-distance measure calculates an interpretation such that the number of distances greater than 0 to the models of each formula is minimal. The value of the inconsistency is than exactly this number of distances.
    Note: This implementation may produce different results than DHitInconsistencyMeasure in a few cases because the latter implements a slightly different interpretation of the measure.
    Author:
    Anna Gessler
    • Constructor Detail

      • DHitSatInconsistencyMeasure

        public DHitSatInconsistencyMeasure​(SatSolver solver)
        Create a new DHitSatInconsistencyMeasure with the given SAT solver.
        Parameters:
        solver - some SAT solver
      • DHitSatInconsistencyMeasure

        public DHitSatInconsistencyMeasure()
        Create a new DHitSatInconsistencyMeasure with the default SAT solver.
    • Method Detail

      • getSATEncoding

        public PlBeliefSet getSATEncoding​(java.util.Collection<PlFormula> kb,
                                          int upper_bound)
      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object