count

Documentation

Overview

Package count provides algorithms for counting models on formulas in LogicNG.

Index

• func Count(fac f.Factory, variables []f.Variable, formulas ...f.Formula) (*big.Int, error)
• func CountWithHandler(fac f.Factory, variables []f.Variable, handler dnnf.Handler, ...) (*big.Int, error, bool)
• func OnFormula(fac f.Factory, formula f.Formula, variables []f.Variable) *big.Int
• func OnFormulaWithConfig(fac f.Factory, formula f.Formula, variables []f.Variable, config *iter.Config) (*big.Int, bool)
• func OnSolver(solver *sat.Solver, variables []f.Variable) *big.Int
• func OnSolverWithConfig(solver *sat.Solver, variables []f.Variable, config *iter.Config) (*big.Int, bool)

Functions

func Count

func Count(fac f.Factory, variables []f.Variable, formulas ...f.Formula) (*big.Int, error)

Count computes the model count for the given formulas (interpreted as conjunction) and a set of relevant variables. This set can only be a superset of the original formulas' variables. No projected model counting is supported. This is just used for don't care variable detection.

Since the counter internally has to generate a CNF formula which does not alter the model count, only AMO and EXO cardinality constraints can be counted - if there are arbitrary cardinality constraints or pseudo-Boolean constraints in the formula, an error is returned.

func CountWithHandler

func CountWithHandler(
	fac f.Factory,
	variables []f.Variable,
	handler dnnf.Handler,
	formulas ...f.Formula,
) (*big.Int, error, bool)

CountWithHandler computes the model count for the given formulas (interpreted as conjunction) and a set of relevant variables. This set can only be a superset of the original formulas' variables. No projected model counting is supported. This is just used for don't care variable detection.

Since the counter internally has to generate a CNF formula which does not alter the model count, only AMO and EXO cardinality constraints can be counted - if there are arbitrary cardinality constraints or pseudo-Boolean constraints in the formula, an error is returned.

If the DNNF handler aborts the dnnf compilation the ok flag is false.

func OnFormula

func OnFormula(fac f.Factory, formula f.Formula, variables []f.Variable) *big.Int

OnFormula counts all models of a formula over the given variables.

func OnFormulaWithConfig

func OnFormulaWithConfig(
	fac f.Factory,
	formula f.Formula,
	variables []f.Variable,
	config *iter.Config,
) (*big.Int, bool)

OnFormulaWithConfig counts all models of a formula over the given variables. The config can be used to influence the model iteration process by setting a handler and/or an iteration strategy.

func OnSolver

func OnSolver(solver *sat.Solver, variables []f.Variable) *big.Int

OnSolver counts all models on the given SAT solver over the given variables.

func OnSolverWithConfig

func OnSolverWithConfig(solver *sat.Solver, variables []f.Variable, config *iter.Config) (*big.Int, bool)

OnSolverWithConfig counts all models on the given SAT solver over the given variables. The config can be used to influence the model iteration process by setting a handler and/or an iteration strategy.