Documentation
¶
Overview ¶
Package mus provides data structures and algorithms for minimal unsatisfiable sets (MUS) in LogicNG.
A MUS contains only those formulas which lead to the given set of formulas being unsatisfiable. In other words: If you remove at least one of the formulas in the MUS from the given set of formulas, your set of formulas is satisfiable. This means a MUS is locally minimal. Thus, given a set of formulas which is unsatisfiable, you can compute its MUS and have one locally minimal conflict description why it is unsatisfiable.
To compute a MUS on a list of propositions, you can call
mus.ComputeInsertionBased(fac, propositions)
or
mus.DeletionInsertionBased(fac, propositions)
Index ¶
- func ComputeDeletionBased(fac f.Factory, propositions *[]f.Proposition) (*e.UnsatCore, error)
- func ComputeDeletionBasedWithHandler(fac f.Factory, propositions *[]f.Proposition, satHandler s.Handler) (unsatCore *e.UnsatCore, ok bool, err error)
- func ComputeInsertionBased(fac f.Factory, propositions *[]f.Proposition) (*e.UnsatCore, error)
- func ComputeInsertionBasedWithHandler(fac f.Factory, propositions *[]f.Proposition, satHandler s.Handler) (unsatCore *e.UnsatCore, ok bool, err error)
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ComputeDeletionBased ¶
ComputeDeletionBased computes a MUS using the deletion-based algorithm. The main idea of this algorithm is to start with all given formulas and iteratively test each formula for relevance. A formula is relevant for the conflict, if its removal yields in a satisfiable set of formulas. Only the relevant formulas are kept.
Returns an error if the formula is satisfiable.
func ComputeDeletionBasedWithHandler ¶
func ComputeDeletionBasedWithHandler( fac f.Factory, propositions *[]f.Proposition, satHandler s.Handler, ) (unsatCore *e.UnsatCore, ok bool, err error)
ComputeDeletionBasedWithHandler computes a MUS using the deletion-based algorithm. The given SAT handler can be used to abort the MUS computation. If the computation was aborted by the handler, the ok flag is false.
Returns an error if the formula is satisfiable.
func ComputeInsertionBased ¶
ComputeInsertionBased computes a MUS using the insertion-based algorithm. The main idea of this algorithm is to start with an empty set and incrementally add propositions to the MUS which have been identified to be relevant.
Returns an error if the formula is satisfiable.
func ComputeInsertionBasedWithHandler ¶
func ComputeInsertionBasedWithHandler( fac f.Factory, propositions *[]f.Proposition, satHandler s.Handler, ) (unsatCore *e.UnsatCore, ok bool, err error)
ComputeInsertionBasedWithHandler computes a MUS using the insertion-based algorithm. The given SAT handler can be used to abort the MUS computation. If the computation was aborted by the handler, the ok flag is false.
Returns an error if the formula is satisfiable.
Types ¶
This section is empty.
Source Files