primeimplicant

Documentation

Overview

Package primeimplicant provides algorithms for computing minimum prime implicants and minimum prime implicant coverages in LogicNG.

• An implicant of a formula is any min-term – a conjunction of literals – such that the implicant logically implies the formula.
• A prime implicant is an implicant which cannot be further reduced (i.e. literals being removed) such that the reduced term yields an implicant.
• A minimum-size prime implicant is a prime implicant with minimum size, in terms of the number of literals, among all prime implicants of a formula.

LogicNG provides a function to compute a minimum prime implicant:

fac := formula.NewFactory()
p := parser.New(fac)
f1 := p.ParseUnsafe("(A | B) & (A | C ) & (C | D) & (B | ~D)")
implicant, err := primimplicant.Minimum(fac, f1) // implicant B, C

A prime implicant cover of a formula is a number of prime implicants which cover all min-terms of the formula. To compute such a cover of minimal size, you can use the following code. Computing minimal prime covers is an important step in simplifying algorithms like QuineMcCluskey.

fac := formula.NewFactory()
p := parser.New(fac)
f1 := p.ParseUnsafe("(A | B) & (A | C ) & (C | D) & (B | ~D)")
primes := primimplicant.CoverMin(fac, f1, primimplicant.CoverImplicants)
implicants := primes.Implicants // [B, C], [A, C, ~D], [A, B, D]

Index

• func Minimum(fac f.Factory, formula f.Formula) ([]f.Literal, error)
• type CoverSort
• type PrimeResult
  • func CoverMax(fac f.Factory, formula f.Formula, coverSort CoverSort) *PrimeResult
  • func CoverMaxWithHandler(fac f.Factory, formula f.Formula, coverSort CoverSort, ...) (*PrimeResult, bool)
  • func CoverMin(fac f.Factory, formula f.Formula, coverSort CoverSort) *PrimeResult
  • func CoverMinWithHandler(fac f.Factory, formula f.Formula, coverSort CoverSort, ...) (*PrimeResult, bool)

Functions

func Minimum

func Minimum(fac f.Factory, formula f.Formula) ([]f.Literal, error)

Minimum computes a minimum-size prime implicant for the given formula. If the formula is unsatisfiable it returns an error.

Types

type CoverSort

type CoverSort byte

CoverSort encodes the sort of the cover: Implicants or Implicates.

const (
	CoverImplicants CoverSort = iota
	CoverImplicates
)

type PrimeResult

type PrimeResult struct {
	Implicants [][]f.Literal
	Implicates [][]f.Literal
	CoverSort  CoverSort
}

PrimeResult gathers the result of a prime implicant computation and holds implicants, implicates, and the cover type.

func CoverMax

func CoverMax(fac f.Factory, formula f.Formula, coverSort CoverSort) *PrimeResult

CoverMax computes prime implicants and prime implicates for a given formula using maximal models. The cover type specifies if the implicants or the implicates will be complete, the other one will still be a cover of the given formula.

func CoverMaxWithHandler

func CoverMaxWithHandler(
	fac f.Factory, formula f.Formula, coverSort CoverSort, optimizationHandler sat.OptimizationHandler,
) (*PrimeResult, bool)

CoverMaxWithHandler computes prime implicants and prime implicates for a given formula using maximal models. The cover type specifies if the implicants or the implicates will be complete, the other one will still be a cover of the given formula. The given handler can be used to abort the SAT-Solver based optimization during the computation.

func CoverMin

func CoverMin(fac f.Factory, formula f.Formula, coverSort CoverSort) *PrimeResult

CoverMin computes prime implicants and prime implicates for a given formula using minimal models. The cover type specifies if the implicants or the implicates will be complete, the other one will still be a cover of the given formula.

func CoverMinWithHandler

func CoverMinWithHandler(
	fac f.Factory, formula f.Formula, coverSort CoverSort, optimizationHandler sat.OptimizationHandler,
) (*PrimeResult, bool)

CoverMinWithHandler computes prime implicants and prime implicates for a given formula using minimal models. The cover type specifies if the implicants or the implicates will be complete, the other one will still be a cover of the given formula. The given handler can be used to abort the SAT-Solver based optimization during the computation.