Interface ConsistencyWitnessProvider<B extends BeliefBase,​S extends Formula>

Type Parameters:
S - The type of formulas.
B - the type of belief bases
All Known Implementing Classes:
CmdLineSatSolver, MaxSatSolver, OpenWboSolver, Sat4jSolver, SatSolver, SimpleDpllSolver

public interface ConsistencyWitnessProvider<B extends BeliefBase,​S extends Formula>
Provides methods for returning some model (if it exists) of a set of formulas.
Author:
Matthias Thimm
  • Method Summary

    Modifier and Type
    Method
    Description
    getWitness​(Collection<S> formulas)
    If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
    getWitness​(BeliefSet<S,​?> bs)
    If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
    getWitness​(S formula)
    If the formula is consistent this method returns some model of it or, if it is inconsistent, null.
  • Method Details

    • getWitness

      Interpretation<B,​S> getWitness(Collection<S> formulas)
      If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
      Parameters:
      formulas - a set of formulas
      Returns:
      some model of the formulas or null.
    • getWitness

      Interpretation<B,​S> getWitness(S formula)
      If the formula is consistent this method returns some model of it or, if it is inconsistent, null.
      Parameters:
      formula - a formula
      Returns:
      some model of the formula or null.
    • getWitness

      Interpretation<B,​S> getWitness(BeliefSet<S,​?> bs)
      If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
      Parameters:
      bs - a belief set
      Returns:
      some model of the belief set or null.