mus

package
v0.4.0 Latest Latest
Warning

This package is not in the latest version of its module.

Go to latest
Published: May 11, 2024 License: MIT Imports: 5 Imported by: 1

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

Constants

This section is empty.

Variables

This section is empty.

Functions

func ComputeDeletionBased

func ComputeDeletionBased(fac f.Factory, propositions *[]f.Proposition) (*e.UnsatCore, error)

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

func ComputeInsertionBased(fac f.Factory, propositions *[]f.Proposition) (*e.UnsatCore, error)

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.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL