Package org.ddolib.examples.max2sat

Class Max2SatProblem

java.lang.Object
org.ddolib.examples.max2sat.Max2SatProblem
All Implemented Interfaces:
Problem<Max2SatState>
public class Max2SatProblem extends Object implements Problem<Max2SatState>
Represents a Maximum 2-Satisfiability (MAX2SAT) problem instance.

In a MAX2SAT problem, each clause involves at most two literals, and each clause has an associated weight. The objective is to find an assignment to the variables that maximizes the sum of the weights of satisfied clauses.

This class implements the Problem interface with states of type Max2SatState. It provides methods for generating the domain of a variable, computing transitions, and evaluating the cost of a transition.

Decision variables are indexed from 0 internally, but the BinaryClause representation requires indices starting from 1. The methods t(int) and f(int) handle this mapping for positive and negated literals, respectively.

See Also:

  • Constructor Details

    • Max2SatProblem

      public Max2SatProblem(int numVar, HashMap<BinaryClause,Integer> weights, Optional<Double> optimal)
      Constructs a MAX2SAT problem instance.
      Parameters:
      numVar - Number of decision variables.
      weights - Map of binary clauses to their weights.
      optimal - Optional known optimal value.

    • Max2SatProblem

      public Max2SatProblem(int numVar, HashMap<BinaryClause,Integer> weights)
      Constructs a MAX2SAT problem instance without specifying an optimal value.
      Parameters:
      numVar - Number of decision variables.
      weights - Map of binary clauses to their weights.

    • Max2SatProblem

      public Max2SatProblem(String fname) throws IOException
      Constructs a MAX2SAT problem instance from a file.

      The file format:

      • First line: number of variables [optimal value (optional)]
      • Subsequent lines: each line is a clause:
        • Unary clause: variable index and weight
        • Binary clause: two variable indices and weight
      Parameters:
      fname - Path to the input file.
      Throws:
      IOException - if the file cannot be read.

  • Method Details

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • nbVars

      public int nbVars()
      Specified by:
      nbVars in interface Problem<Max2SatState>
      Returns:
      the total number of decision variables in this problem

    • initialState

      public Max2SatState initialState()
      Description copied from interface: Problem
      Returns the initial state of the problem.
      Specified by:
      initialState in interface Problem<Max2SatState>
      Returns:
      the state representing the starting point of the optimization

    • initialValue

      public double initialValue()
      Computes the initial value of the problem.

      Unary clauses of the form (x_i OR NOT x_i) are always satisfied, so their weight is added directly at the start.

      Specified by:
      initialValue in interface Problem<Max2SatState>
      Returns:
      the initial value

    • domain

      public Iterator<Integer> domain(Max2SatState state, int var)
      Description copied from interface: Problem
      Returns the domain of possible values for a given variable when applied to a specific state.
      Specified by:
      domain in interface Problem<Max2SatState>
      Parameters:
      state - the current state
      var - the variable index whose domain is queried
      Returns:
      an iterator over all feasible values for the variable in this state

    • transition

      public Max2SatState transition(Max2SatState state, Decision decision)
      Description copied from interface: Problem
      Applies a decision to a state, computing the next state according to the problem's transition function.
      Specified by:
      transition in interface Problem<Max2SatState>
      Parameters:
      state - the state from which the transition originates
      decision - the decision to apply
      Returns:
      the resulting state after applying the decision

    • transitionCost

      public double transitionCost(Max2SatState state, Decision decision)
      Description copied from interface: Problem
      Computes the change in objective value resulting from applying a decision to a given state.
      Specified by:
      transitionCost in interface Problem<Max2SatState>
      Parameters:
      state - the state from which the transition originates
      decision - the decision to apply
      Returns:
      the incremental objective cost/value associated with this decision

    • optimalValue

      public Optional<Double> optimalValue()
      Description copied from interface: Problem
      Returns the known optimal value of the problem, if available.

      Note: This value should correspond to the expected output of the solver. For maximization problems, be careful with negative values.

      Specified by:
      optimalValue in interface Problem<Max2SatState>
      Returns:
      an Optional containing the known optimal value, or empty if unknown

    • evaluate

      public double evaluate(int[] solution) throws InvalidSolutionException
      Description copied from interface: Problem
      Given a solution such that solution[i] is the value of the variable x_i, returns the value of this solution and checks if the solution respects the problem's constraints.

      Note: For maximization problems, the returned value is minus the computed value.

      Specified by:
      evaluate in interface Problem<Max2SatState>
      Parameters:
      solution - A solution of the problem.
      Returns:
      The value of the input solution
      Throws:
      InvalidSolutionException - If the solution does not respect problem's constraints.

    • t

      public int t(int x)
      Returns the positive literal for a variable.
      Parameters:
      x - variable index
      Returns:
      value representing x_i

    • f

      public int f(int x)
      Returns the negated literal for a variable.
      Parameters:
      x - variable index
      Returns:
      value representing NOT x_i

    • weight

      public int weight(int x, int y)
      Returns the weight of a binary clause (x, y), considering commutativity.
      Parameters:
      x - first literal
      y - second literal
      Returns:
      weight of the clause, or 0 if absent