Documentation
¶
Overview ¶
Package smus provides an algorithm to compute a smallest minimal unsatisfiable set (SMUS) of a set of propositions or formulas in LogicNG.
A smallest minimal unsatisfiable set (SMUS) is a smallest MUS based on the number of formulas it contains. So in contrast to a regular MUS it is not only locally minimal, but globally minimal.
The implementation in LogicNG is based on "Smallest MUS extraction with minimal hitting set dualization" (Ignatiev, Previti, Liffiton & Marques-Silva, 2015).
To compute a SMUS on a list of propositions you can call
smus.Compute(fac, propositions)
Index ¶
- func Compute(fac f.Factory, propositions []f.Proposition, ...) []f.Proposition
- func ComputeForFormulas(fac f.Factory, formulas []f.Formula, additionalConstraints ...f.Formula) []f.Formula
- func ComputeForFormulasWithHandler(fac f.Factory, formulas []f.Formula, ...) (smus []f.Formula, ok bool)
- func ComputeWithHandler(fac f.Factory, propositions []f.Proposition, ...) (smus []f.Proposition, ok bool)
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Compute ¶
func Compute( fac f.Factory, propositions []f.Proposition, additionalConstraints ...f.Formula, ) []f.Proposition
Compute computes the SMUS for the given list of propositions modulo some additional constraints. Returns the SMUS as a list of propositions.
func ComputeForFormulas ¶
func ComputeForFormulas( fac f.Factory, formulas []f.Formula, additionalConstraints ...f.Formula, ) []f.Formula
ComputeForFormulas computes the SMUS for the given list of formulas modulo some additional constraints. Returns the SMUS as a list of formulas.
func ComputeForFormulasWithHandler ¶
func ComputeForFormulasWithHandler( fac f.Factory, formulas []f.Formula, optimizationHandler sat.OptimizationHandler, additionalConstraints ...f.Formula, ) (smus []f.Formula, ok bool)
ComputeForFormulasWithHandler computes the SMUS for the given list of formulas modulo some additional constraints. The optimization handler can be used to abort the computation. Returns the SMUS as a list of formulas. If the handler aborted the computation, the ok flag is false.
func ComputeWithHandler ¶
func ComputeWithHandler( fac f.Factory, propositions []f.Proposition, optimizationHandler sat.OptimizationHandler, additionalConstraints ...f.Formula, ) (smus []f.Proposition, ok bool)
ComputeWithHandler computes the SMUS for the given list of propositions modulo some additional constraints. The optimization handler can be used to abort the computation. Returns the SMUS as a list of propositions. If the handler aborted the computation, the ok flag is false.
Types ¶
This section is empty.
Source Files