Class WeightedCnfProblem

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Formats.dll

A weighted partial MaxSAT problem parsed from WCNF: hard clauses that must hold and soft clauses that carry a positive weight, the total weight of the falsified softs being minimized. Hands off directly to the in-house MaxSatSolver. Top is the hard-clause weight sentinel of the classic format, preserved so the writer round-trips.

public sealed class WeightedCnfProblem

Inheritance

object

WeightedCnfProblem

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Properties

HardClauses

Hard clauses that any feasible assignment must satisfy.

public IReadOnlyList<int[]> HardClauses { get; }

Property Value

IReadOnlyList<int[]>

SoftClauses

Soft clauses paired with the positive weight paid when they are falsified.

public IReadOnlyList<(long Weight, int[] Literals)> SoftClauses { get; }

Property Value

IReadOnlyList<(long Weight, int[] Literals)>

Top

The hard-clause weight sentinel (classic p wcnf n m top header).

public long Top { get; }

Property Value

long

VariableCount

Declared number of variables (indices 1..VariableCount).

public int VariableCount { get; }

Property Value

int

Methods

Solve(int, CancellationToken)

Optimize this instance with the in-house weighted partial MaxSAT solver.

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

Parameters

maxConflictsPerCall int

cancellationToken CancellationToken

Returns

MaxSatResult

ToSolver()

Build a MaxSatSolver loaded with every hard and soft clause.

public MaxSatSolver ToSolver()

Returns

MaxSatSolver

Write(TextWriter)

Write this problem back out as classic WCNF text (round-trips through the parser): a p wcnf n m top header, then top ... 0 hard clauses and weight ... 0 soft clauses.

public void Write(TextWriter writer)

Parameters

writer TextWriter