Package org.ddolib.examples.max2sat

Class BinaryClause

java.lang.Object
org.ddolib.examples.max2sat.BinaryClause
All Implemented Interfaces:
Comparable<BinaryClause>
public class BinaryClause extends Object implements Comparable<BinaryClause>
Class to model a Binary clause of two literals for CNF formula.

To symbolize a literal x_i , for i > 0, we give the value i as input. To symbolize NOT x_i, we give -i.

  • Field Details

    • i

      public final int i

    • j

      public final int j

  • Constructor Details

    • BinaryClause

      public BinaryClause(int i, int j)

  • Method Details

    • eval

      public int eval(int a, int b)
      Evaluates if the clause is verified given 2 boolean values.
      Parameters:
      a - The value to attribute to the variable x_i (0 or 1).
      b - The value to attribute to the variable x_j (0 or 1).
      Returns:
      1 if the clause is verified. 0 else.

    • equals

      public boolean equals(Object obj)
      Overrides:
      equals in class Object

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • compareTo

      public int compareTo(BinaryClause other)
      Used to compare binary clauses. It is used to sort them when generating Max2Sat instances.
      The induced order is the following:
      1. The lexical order on the literals' indices.
      2. The positive literal before the negative ones.
      Specified by:
      compareTo in interface Comparable<BinaryClause>
      Parameters:
      other - The binary clause to be compared.
      Returns:
      • 0 if if this == other
      • 1 if this > other
      • -1 if this < other