Class MaxSatSolver

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

Weighted partial MaxSAT: hard clauses must hold, soft clauses carry positive weights and the total weight of falsified softs is minimized. Two algorithms are available (see MaxSatAlgorithm):

• Linear — each soft clause gets a relaxation literal and a linear search tightens a pseudo-Boolean bound on the relaxation weights until UNSAT proves optimality;
• CoreGuided — an MSU3-style lower-bound search that solves under soft-selector assumptions, extracts UNSAT cores and relaxes only the cores with a cardinality / pseudo-Boolean bound raised round by round.

Built entirely on the in-house solver and encoders — no dependencies. Either algorithm, run to completion, returns the same PROVEN optimum; an incumbent found under a spent budget is reported as Unknown, never as Optimal.

public sealed class MaxSatSolver

Inheritance

object

MaxSatSolver

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Constructors

MaxSatSolver(int)

public MaxSatSolver(int variableCount)

Parameters

variableCount int

Methods

AddHard(params int[])

public void AddHard(params int[] literals)

Parameters

literals int[]

AddSoft(int, params int[])

public void AddSoft(int weight, params int[] literals)

Parameters

weight int

literals int[]

Solve(MaxSatAlgorithm, int, CancellationToken)

Solve with the requested algorithm. The parameterless Solve(int, CancellationToken) is preserved and keeps running the linear search; the core-guided path is opt-in through this overload.

public MaxSatResult Solve(MaxSatAlgorithm algorithm, int maxConflictsPerCall = 1000000, CancellationToken cancellationToken = default)

Parameters

algorithm MaxSatAlgorithm

maxConflictsPerCall int

cancellationToken CancellationToken

Returns

MaxSatResult

Solve(int, CancellationToken)

Solve with the linear search (unchanged since the first release). Equivalent to Solve(MaxSatAlgorithm, int, CancellationToken) with Linear.

public MaxSatResult Solve(int maxConflictsPerCall = 1000000, CancellationToken cancellationToken = default)

Parameters

maxConflictsPerCall int

cancellationToken CancellationToken

Returns

MaxSatResult