Enum MaxSatAlgorithm
- Namespace
- LogicalOptimizer
- Assembly
- LogicalOptimizer.Sat.dll
Which MaxSAT search the solver runs. All values return the SAME proven optimum on the instances they solve to completion; they differ only in the search path (and therefore in which instances stay within a given conflict budget).
public enum MaxSatAlgorithmFields
Auto = 0Let the solver choose. Currently routes to Linear (the stable default); the routing may change between minor releases, but only ever between algorithms that return the same proven optimum, and never at the cost of correctness.
CoreGuided = 2Core-guided (unweighted MSU3 / weighted MSU3-style) lower-bound search: solve under soft-selector assumptions, extract UNSAT cores, relax them with a cardinality (pseudo-Boolean when weighted) bound that is raised one round at a time until the formula becomes SAT — at which point the bound is a proven optimum.
Linear = 1The model-improving linear search: tighten a pseudo-Boolean upper bound on the relaxation weights until UNSAT proves optimality. This is exactly what the parameterless Solve(int, CancellationToken) runs.