Package org.ddolib.examples.max2sat

Class Max2SatAstarMain

java.lang.Object

org.ddolib.examples.max2sat.Max2SatAstarMain

public final class Max2SatAstarMain
extends Object

Maximum 2-Satisfiability (MAX2SAT) (MAX2SAT) problem with AsTar. Entry point for solving the Maximum 2-Satisfiability (MAX2SAT) problem using the A* search algorithm.

The A* algorithm explores the search space by expanding states in order of increasing estimated total cost (i.e., actual cost + heuristic lower bound). It guarantees finding an optimal solution when the heuristic is admissible.

Usage:

• If no command-line argument is provided, the default instance file data/Max2Sat/wcnf_var_4_opti_39.txt is used.
• Otherwise, the first argument should specify the path to a Weighted CNF (WCNF) instance file.

Example:

 java Max2SatAstarMain data/Max2Sat/wcnf_var_20_opti_110.txt
 

The program prints each solution found by the A* algorithm via the SolutionPrinter utility, followed by overall search statistics such as number of explored nodes, best cost, and runtime.

See Also:

• Max2SatProblem
• Max2SatState
• Max2SatFastLowerBound
• Solvers.minimizeAstar(Model, java.util.function.BiConsumer)
• SearchStatistics

Constructor Summary

Constructors

Constructor	Description
Max2SatAstarMain()

Method Summary

Modifier and Type	Method	Description
static void	main(String[] args)	Main entry point for executing the A* search on a MAX2SAT instance.

Methods inherited from class java.lang.Object

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

Constructor Details

Max2SatAstarMain

public Max2SatAstarMain()

Method Details

main

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

Main entry point for executing the A* search on a MAX2SAT instance.

Parameters:

args - optional command-line argument specifying the path to the WCNF instance file; if omitted, a default instance file is used.

Throws:

IOException - if the instance file cannot be found, opened, or parsed.