Package org.ddolib.examples.max2sat

Class Max2SatLnsMain

java.lang.Object

org.ddolib.examples.max2sat.Max2SatLnsMain

public class Max2SatLnsMain
extends Object

Entry point for solving the Maximum 2-Satisfiability (MAX-2SAT) problem using a Large Neighborhood Search (LNS) approach combined with Decision Diagram Optimization (DDO).

The MAX-2SAT problem consists in assigning boolean values to variables in order to maximize the number (or total weight) of satisfied clauses, where each clause contains at most two literals.

This class demonstrates how to:

• Load a MAX-2SAT instance from a file (typically in WCNF format)
• Define a LnsModel with problem-specific components
• Use a lower bound heuristic to guide the search
• Run a Large Neighborhood Search (LNS) optimization
• Print intermediate and final solutions

Execution

The program accepts an optional command-line argument specifying the path to a MAX-2SAT instance file. If not provided, a default instance is loaded from:

 data/Max2Sat/wcnf_var_4_opti_39.txt
 

Model Components

• Max2SatProblem – defines the MAX-2SAT instance
• Max2SatFastLowerBound – provides a fast lower bound on the number of satisfiable clauses
• Max2SatRanking – ranks states during decision diagram compilation

Search Configuration

• Search strategy: Large Neighborhood Search (LNS)
• Time limit: 100 milliseconds

No dominance rule or width heuristic is explicitly specified, so default behaviors (if provided by the framework) are used.

Output

The program prints:

• Intermediate solutions during the search
• Final solution statistics
• The best assignment found

See Also:

• Max2SatProblem
• Max2SatState
• Max2SatFastLowerBound
• Max2SatRanking
• LnsModel
• Solvers.minimizeLns(org.ddolib.modeling.LnsModel<T>, java.util.function.Predicate<org.ddolib.common.solver.SearchStatistics>, java.util.function.BiConsumer<int[], org.ddolib.common.solver.SearchStatistics>)
• Solution

Constructor Summary

Constructors

Constructor	Description
Max2SatLnsMain()

Method Summary

Modifier and Type	Method	Description
static void	main(String[] args)	Main entry point of the program.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

Max2SatLnsMain

public Max2SatLnsMain()

Method Details

main

public static void main(String[] args)
                 throws IOException

Main entry point of the program.

Loads a MAX-2SAT instance, configures the LNS model with problem-specific heuristics, and runs the optimization process.

Parameters:

args - optional command-line arguments:

• args[0] – path to the MAX-2SAT instance file

Throws:

IOException - if the instance file cannot be read