Class Sat4jSolver

All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

public class Sat4jSolver extends DimacsSatSolver
Uses the Sat4j library for SAT solving (note that currently only the light version is used).
Author:
Matthias Thimm
  • Constructor Details

    • Sat4jSolver

      public Sat4jSolver(int maxvar, int nbclauses)
      Creates a new solver with the given parameters.
      Parameters:
      maxvar - Max number of variables for this solver.
      nbclauses - Max number of expected clauses for this solver.
    • Sat4jSolver

      public Sat4jSolver()
      Creates a new solver with default parameters (maxvar=1000000, nbclauses=500000).
  • Method Details

    • isSatisfiable

      public boolean isSatisfiable(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, String additional_clauses, int num_additional_clauses)
      Description copied from class: DimacsSatSolver
      Checks whether the given set of formulas is satisfiable.
      Specified by:
      isSatisfiable in class DimacsSatSolver
      Parameters:
      formulas - a set of formulas.
      prop_index - maps propositions to the number that shall be used to represent it (a natural number > 0).
      additional_clauses - additional clauses in text form to be added (already correctly formatted in CNF!)
      num_additional_clauses - the number of additional_clauses
      Returns:
      "true" if the set is consistent.
    • getWitness

      public Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index, String additional_clauses, int num_additional_clauses)
      Description copied from class: DimacsSatSolver
      If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
      Specified by:
      getWitness in class DimacsSatSolver
      Parameters:
      formulas - a set of formulas
      prop_index - mapping propositions to numbers used for representing the SAT instance
      prop_inverted_index - inverted index of prop_index
      additional_clauses - additional clauses in text form to be added (already correctly formatted in CNF!)
      num_additional_clauses - the number of additional_clauses
      Returns:
      some model of the formulas or null.
    • isInstalled

      public boolean isInstalled()
      Specified by:
      isInstalled in class DimacsSatSolver
      Returns:
      whether the solve ris installed