Package org.jacop.satwrapper

Class SatWrapper

java.lang.Object
org.jacop.constraints.DecomposedConstraint<Constraint>
org.jacop.constraints.Constraint
org.jacop.satwrapper.SatWrapper
All Implemented Interfaces:
SatisfiedPresent, Stateful, SolverComponent, ConflictListener, ExplanationListener, SolutionListener, StartStopListener
public final class SatWrapper extends Constraint implements ConflictListener, ExplanationListener, StartStopListener, SolutionListener, Stateful, SatisfiedPresent
wrapper to communicate between SAT solver and CP solver. It listens for SAT conflicts, so that it can force the CP solver to backtrack until the conflict is resolved in SAT. It listens to propagations, to know which literals are asserted in SAT, to report those assertions on CP variables domains.
Version:
4.10

  • Field Details

    • empty

      boolean empty

    • core

      public Core core

    • activity

      public ActivityModule activity

    • assertionModule

      public HeuristicAssertionModule assertionModule

    • boolVarToDomains

      public SatCPBridge[] boolVarToDomains

    • satChangesListener

      public SatChangesListener satChangesListener

    • store

      public Store store

    • pool

      public MemoryPool pool

    • domainDatabase

      public DomainClausesDatabase domainDatabase

    • domainTranslator

      public DomainTranslator domainTranslator

    • registeredVars

      public final Set<IntVar> registeredVars

    • levelToBackjumpTo

      public int levelToBackjumpTo

    • satToCpLevels

      public Integer[] satToCpLevels

    • cpToSatLevels

      public Integer[] cpToSatLevels

    • verbosity

      public int verbosity

    • trail

      private Trail trail

    • currentSatLevel

      private int currentSatLevel

    • modelClausesToAdd

      private final ArrayDeque<int[]> modelClausesToAdd

    • toAssertLiterals

      private IntQueue toAssertLiterals

    • clauseToLearn

      private MapClause clauseToLearn

    • mustBacktrack

      private boolean mustBacktrack

    • hasSolution

      private boolean hasSolution

  • Constructor Details

    • SatWrapper

      public SatWrapper()
      creates everything in the right order

  • Method Details

    • register

      public void register(IntVar result)

    • register

      public void register(IntVar variable, boolean translate)
      registers the variable so that we can use it in SAT solver
      Parameters:
      variable - the CP IntVar variable
      translate - indicate whether to use == or <=

    • consistency

      public void consistency(Store store)
      The point where all operations are effectively done in the SAT solver, until no operation remains or a conflict occurs
      Specified by:
      consistency in class Constraint
      Parameters:
      store - constraint store within which the constraint consistency is being checked.

    • processOneLiteral

      private void processOneLiteral()
      assert the next literal from toAssertLiterals

    • addSatLevel

      private void addSatLevel()
      adds one level for SAT side, and remembers the association between CP and SAT levels

    • onConflict

      public void onConflict(MapClause clause, int level)
      wrapper listens for conflicts.
      Specified by:
      onConflict in interface ConflictListener
      Parameters:
      clause - the conflict (unsatisfiable) clause
      level - the level at which the conflict occurred

    • onExplain

      public void onExplain(MapClause explanation)
      wrapper listens for explanations, to know how deep to backtrack
      Specified by:
      onExplain in interface ExplanationListener
      Parameters:
      explanation - the explanation clause

    • onSolution

      public void onSolution(boolean satisfiable)
      Description copied from interface: SolutionListener
      a handler called when a solution is found.
      Specified by:
      onSolution in interface SolutionListener
      Parameters:
      satisfiable - true when the solution is Satisfiable, false if it is Unsatisfiable.

    • removeLevel

      public void removeLevel(int cpLevel)
      when the CP solver decides to remove a level, the wrapper must force the SAT solver to backtrack accordingly, to keep mappings between the two search trees consistent. This is also the place where the wrapper can decide that a conflict in the SAT solver has been solved.
      Specified by:
      removeLevel in interface Stateful
      Parameters:
      cpLevel - the level which is being removed.

    • queueVariable

      public void queueVariable(int level, Var var)
      Description copied from class: Constraint
      This is a function called to indicate which variable in a scope of constraint has changed. It also indicates a store level at which the change has occurred.
      Overrides:
      queueVariable in class Constraint
      Parameters:
      level - the level of the store at which the change has occurred.
      var - variable which has changed.

    • setBoolVariable

      private void setBoolVariable(int variable, boolean value)
      called when a boolean variable is set to some boolean value
      Parameters:
      variable - the boolean variable
      value - the value (true or false) of this variable

    • getConsistencyPruningEvent

      public int getConsistencyPruningEvent(Var var)
      Description copied from class: Constraint
      It retrieves the pruning event which causes reevaluation of the constraint.
      Overrides:
      getConsistencyPruningEvent in class Constraint
      Parameters:
      var - variable for which pruning event is retrieved
      Returns:
      it returns the int code of the pruning event (GROUND, BOUND, ANY, NONE)

    • getDefaultConsistencyPruningEvent

      public int getDefaultConsistencyPruningEvent()
      Specified by:
      getDefaultConsistencyPruningEvent in class Constraint

    • getMostActiveLiteral

      public int getMostActiveLiteral()
      asks the solver for which literal is the most active. It will return a literal, which can be transformed into a variable and a value from the variable domain. Useful when the CP solver does not know which variable to set to continue research
      Returns:
      a literal corresponding to some possible (variable,value)

    • showLiteralMeaning

      public String showLiteralMeaning(int literal)
      (for debug) show what a literal means
      Parameters:
      literal - literal for showing its meaning
      Returns:
      literal meaning

    • showClauseMeaning

      public String showClauseMeaning(Iterable<Integer> literals)

    • id

      public String id()
      Description copied from class: Constraint
      It gives the id string of a constraint.
      Overrides:
      id in class Constraint
      Returns:
      string id of the constraint.

    • removeConstraint

      public void removeConstraint()
      Description copied from class: Constraint
      It removes the constraint by removing this constraint from all variables.
      Overrides:
      removeConstraint in class Constraint

    • satisfied

      public boolean satisfied()
      Description copied from interface: SatisfiedPresent
      It checks if the constraint is satisfied. It can return false even if constraint is satisfied but not all variables in its scope are grounded. It needs to return true if all variables in its scope are grounded and constraint is satisfied.

      Implementations of this interface for constraints that are not PrimitiveConstraint may require constraint imposition and consistency check as a requirement to work correctly.

      Specified by:
      satisfied in interface SatisfiedPresent
      Returns:
      true if constraint is possible to verify that it is satisfied.

    • toString

      public String toString()
      Description copied from class: Constraint
      It produces a string representation of a constraint state.
      Overrides:
      toString in class Constraint

    • increaseWeight

      public void increaseWeight()
      Description copied from class: Constraint
      It increases the weight of the variables in the constraint scope.
      Overrides:
      increaseWeight in class Constraint

    • arguments

      public Set<Var> arguments()
      Description copied from class: Constraint
      It returns the variables in a scope of the constraint.
      Overrides:
      arguments in class Constraint
      Returns:
      variables in a scope of the constraint.

    • addSolverComponent

      public final void addSolverComponent(SolverComponent module)
      to add some module to the solver
      Parameters:
      module - the module to add

    • addWrapperComponent

      public final void addWrapperComponent(WrapperComponent module)
      add a component
      Parameters:
      module - the component

    • forget

      public final void forget()
      asks the solver to forget useless clauses, to free memory

    • addModelClause

      public final void addModelClause(Collection<Integer> clause)
      add model (globally valid) clause to solver, in a delayed fashion
      Parameters:
      clause - the clause to add

    • addModelClause

      public final void addModelClause(int[] clause)

    • impose

      public final void impose(Constraint constraint)
      add the constraint to the wrapper (ie, constraint.imposeToSat(this))
      Parameters:
      constraint - the constraint to add

    • impose

      public final void impose(Store store)
      Description copied from class: Constraint
      It imposes the constraint in a given store.
      Overrides:
      impose in class Constraint
      Parameters:
      store - the constraint store to which the constraint is imposed to.

    • cpVarToBoolVar

      public final int cpVarToBoolVar(IntVar variable, int value, boolean isEquality)
      given a CP variable and a value, retrieve the associated boolean literal for either 'variable = value' or either 'variable <= value'
      Parameters:
      variable - the CP variable
      value - a value in the range of this variable
      isEquality - a boolean, true if we want the literal that stands for 'x=d', false for 'x<=d'
      Returns:
      the corresponding literal, or 0 if it is out of bounds

    • boolVarToDomain

      public final SatCPBridge boolVarToDomain(int literal)
      returns the CpVarDomain associated with this literal
      Parameters:
      literal - the boolean literal
      Returns:
      a range

    • boolVarToCpVar

      public final IntVar boolVarToCpVar(int literal)
      get the IntVar back from a literal
      Parameters:
      literal - the literal
      Returns:
      IntVar represented by the literal

    • boolVarToCpValue

      public final int boolVarToCpValue(int literal)
      transform a literal 'x=v' into a value 'v' for some CP variable
      Parameters:
      literal - literal to be transformed to value it represents
      Returns:
      the value represented by this literal

    • isEqualityBoolVar

      public final boolean isEqualityBoolVar(int literal)
      checks if the boolean variable represents an assertion 'x=v' or 'x<=v'
      Parameters:
      literal - the boolean literal
      Returns:
      true if the literal represents a proposition 'x=v', false if it represents 'x<=v'

    • isVarLiteral

      public final boolean isVarLiteral(int literal)
      checks if this literal corresponds to some CP variable
      Parameters:
      literal - the literal
      Returns:
      true if this literal stands for some 'x=v' or 'x<=v' proposition

    • log

      public boolean log(Object o, String format, Object... args)
      log method, similar to printf. Example: wrapper.log(this, "%s is %d", "foo", 42);
      Parameters:
      o - the object that logs something (use this)
      format - the format string (the message, if no formatting)
      args - the arguments to fill in the format
      Returns:
      always true

    • onStart

      public void onStart()
      Description copied from interface: StartStopListener
      called when the solver starts search. It will be called only once.
      Specified by:
      onStart in interface StartStopListener

    • onStop

      public void onStop()
      Description copied from interface: StartStopListener
      called when the solver stop search, for any reason
      Specified by:
      onStop in interface StartStopListener

    • initialize

      public void initialize(Core core)
      Description copied from interface: SolverComponent
      initializes the component with the given solver. May be called only once. This method must register the component to the solver for the run.
      Specified by:
      initialize in interface SolverComponent
      Parameters:
      core - core component to initialize

    • toCNF

      public void toCNF(BufferedWriter output) throws IOException
      Throws:
      IOException