Package org.ddolib.examples.max2sat

package org.ddolib.examples.max2sat

This package implements the acs, astar and ddo models for the Maximum 2-Satisfiability Problem (MAX2SAT) Problem. Given a logic formula in CNF whose clauses (of the formula comprises at most two literals) have each been assigned a weight, the MAX2SAT problem consists in finding a variable assignment that maximizes the total weight of the satisfied clauses. This problem is considered in the papers:

• David Bergman et al. Decision Diagrams for Optimization. Ed. by Barry O’Sullivan and Michael Wooldridge. Springer, 2016.
• David Bergman et al. “Discrete Optimization with Decision Diagrams”. In: INFORMS Journal on Computing 28.1 (2016), pp. 47–66.

Related Packages

Package	Description
org.ddolib.examples	Package containing examples

Class	Description
BinaryClause	Class to model a Binary clause of two literals for CNF formula.
Max2SatAcsMain	Maximum 2-Satisfiability (MAX2SAT) (MAX2SAT) problem with Acs.
Max2SatAstarMain	Maximum 2-Satisfiability (MAX2SAT) (MAX2SAT) problem with AsTar.
Max2SatDdoMain	Maximum 2-Satisfiability (MAX2SAT) (MAX2SAT) problem with Ddo.
Max2SatFastLowerBound	Implementation of a fast lower bound heuristic for the Maximum 2-Satisfiability (MAX2SAT) problem.
Max2SatGenerator	Methods to generate random instance of the Max2Sat problem.
Max2SatLnsMain	Entry point for solving the Maximum 2-Satisfiability (MAX-2SAT) problem using a Large Neighborhood Search (LNS) approach combined with Decision Diagram Optimization (DDO).
Max2SatProblem	Represents a Maximum 2-Satisfiability (MAX2SAT) problem instance.
Max2SatRanking	Class used to compare two states for the Max2Sat problem.
Max2SatRelax	Implements a relaxation for the Maximum 2-Satisfiability (MAX2SAT) problem.
Max2SatState	Class to contain data for the Max2Sat sate.
NaiveMax2SatSolver	A naive Max2Sat solver which enumerates all the solution to find the best one.