encoding

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: 6 Imported by: 1

Documentation

Overview

Package encoding provides data structures and algorithms for cardinality and pseudo-Boolean encodings in LogicNG.

Encoders transform a constraint into a CNF representation. For conventional (non-incremental) cardinality constraints we have the following encodings for AMO (at-most-one), EXO (exactly-one), AMK (at-most-k), ALK (at-least-k) constraints, and EXK (exactly-k):

  • Pure (AMO, EXO): 'naive' encoding with no introduction of new variables but quadratic size
  • Ladder (AMO, EXO): Ladder/Regular Encoding due to Gent & Nightingale
  • Product (AMO, EXO): the 2-Product Method due to Chen
  • Nested (AMO, EXO): Nested pure encoding
  • Commander (AMO, EXO): Commander Encoding due to Klieber & Kwon
  • Binary (AMO, EXO): Binary Encoding due to Doggett, Frisch, Peugniez, and Nightingale
  • Bimander (AMO, EXO): Bimander Encoding due to Hölldobler and Nguyen
  • Cardinality Network (AMK, ALK, EXK): Cardinality Network Encoding due to Asín, Nieuwenhuis, Oliveras, and Rodríguez-Carbonell
  • Totalizer (AMK, ALK, EXK): Totalizer Encoding due to Bailleux and Boufkhad
  • Modulo Totalizer (AMK, ALK): Modulo Totalizer due to Ogawa, Liu, Hasegawa, Koshimura & Fujita

Incremental cardinality constraints are a special variant of encodings, where the upper/lower bound of the constraint can be tightened by adding additional clauses to the resulting CNF. All AMK and ALK encodings support incremental encodings.

For pseudo-Boolean constraints there are three different encodings:

  • PBAdderNetworks: Adder networks encoding
  • PBSWC: A sequential weight counter for the encoding of pseudo-Boolean constraints in CNF
  • PBBinaryMerge: Binary merge due to Manthey, Philipp, and Steinke

To encode a constraint explicitly (and not implicitly within e.g. the CNF methods) you can use the following code: 

fac := formula.NewFactory()
cc := fac.AMO(fac.Vars("a", "b", "c", "d")...) // a + b + c + d <= 1
encoding, err := encoding.EncodeCC(fac, cc)

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func ContainsPBC 

func ContainsPBC(fac f.Factory, formula f.Formula) bool

ContainsPBC reports whether the given formula contains a pseudo-Boolean constraint of any sort.

func EncodeCC 

func EncodeCC(fac f.Factory, constraint f.Formula, config ...*Config) ([]f.Formula, error)

EncodeCC encodes a cardinality constraint to a CNF formula as a list of clauses.

Depending on the type of cardinality constraint it uses the encoding algorithm as specified either in the optional given config or if it not present the one configured in the formula factory.

Returns an error if the input constraint is no valid cardinality constraint.

func EncodeCCInResult 

func EncodeCCInResult(
	fac f.Factory,
	constraint f.Formula,
	result Result,
	config ...*Config,
) error

EncodeCCInResult encodes a cardinality constraint into an encoding result. This result can be either a formula result and a formula is generated or it can be a solver encoding and the cnf is added directly to the solver without first generating formulas on the formula factory.

Depending on the type of cardinality constraint it uses the encoding algorithm as specified either in the optional given config or if it not present the one configured in the formula factory.

Returns an error if the input constraint is no valid cardinality constraint.

func EncodePBC 

func EncodePBC(fac f.Factory, pbc f.Formula, config ...*Config) ([]f.Formula, error)

EncodePBC encodes a pseudo-Boolean constraint to a CNF formula as a list of clauses. This function can also be called with a cardinality constraint.

It uses the encoding algorithm as specified either in the optional given config or if it not present the one configured in the formula factory.

Returns an error if the input constraint is no valid pseudo-Boolean constraint.

func EncodePBCInResult 

func EncodePBCInResult(fac f.Factory, pbc f.Formula, result Result, config ...*Config) error

EncodePBCInResult encodes a pseudo-Boolean constraint into an encoding result. This result can be either a formula result and a formula is generated or it can be a solver encoding and the cnf is added directly to the solver without first generating formulas on the formula factory.

It uses the encoding algorithm as specified either in the optional given config or if it not present the one configured in the formula factory.

Returns an error if the input constraint is no valid pseudo-Boolean constraint.

func NegatePBC 

func NegatePBC(fac f.Factory, formula f.Formula) f.Formula

NegatePBC returns the negation of the given pseudo-Boolean constraint. In case of LE, LT, GE, GT the negation is computed by negating the comparator. In case of EQ the negation is computed by negating the whole constraint. Panics if the given constraint is not valid on the factory.

func Normalize 

func Normalize(fac f.Factory, constraint f.Formula) f.Formula

Normalize returns a normalized <= constraint of the given pseudo-Boolean or cardinality constraint. Panics if the given constraint is not valid on the factory.

Types

type ALKEncoder 

type ALKEncoder byte
const (
	ALKTotalizer ALKEncoder = iota
	ALKModularTotalizer
	ALKCardinalityNetwork
	ALKBest
)

CcAlkEncoder represents the different algorithms for encoding an at-least-k constraint (ALK) to a CNF.

func (ALKEncoder) String 

func (i ALKEncoder) String() string

type AMKEncoder 

type AMKEncoder byte
const (
	AMKTotalizer AMKEncoder = iota
	AMKModularTotalizer
	AMKCardinalityNetwork
	AMKBest
)

CcAmkEncoder represents the different algorithms for encoding an at-most-k constraint (AMK) to a CNF.

func (AMKEncoder) String 

func (i AMKEncoder) String() string

type AMOEncoder 

type AMOEncoder byte
const (
	AMOPure AMOEncoder = iota
	AMOLadder
	AMOProduct
	AMONested
	AMOCommander
	AMOBinary
	AMOBimander
	AMOBest
)

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

func (AMOEncoder) String 

func (i AMOEncoder) String() string

type BimanderGroupSize 

type BimanderGroupSize byte
const (
	BimanderHalf BimanderGroupSize = iota
	BimanderSqrt
	BimanderFixed
)

BimanderGroupSize is a parameter which can be used for defining the group size in the Bimander encoding for AMO constraints.

func (BimanderGroupSize) String 

func (i BimanderGroupSize) String() string

type CCIncrementalData 

type CCIncrementalData struct {
	Result Result // encoding result of the incremental constraint
	// contains filtered or unexported fields
}

CCIncrementalData gathers data for an incremental at-most-k cardinality constraint. When an at-most-k cardinality constraint is constructed, it is possible to save incremental data with it. Then one can modify the constraint after it was created by tightening the original bound.

func EncodeIncremental 

func EncodeIncremental(
	fac f.Factory,
	constraint f.Formula,
	result Result,
	config ...*Config,
) (*CCIncrementalData, error)

EncodeIncremental encodes an incremental cardinalityConstraint into an encoding result and return the incremental data with this result. This result can be either a formula result and a formula is generated or it can be a solver encoding and the cnf is added directly to the solver without first generating formulas on the formula factory. The returned incremental data can then be used to tighten the bound of the constraint (either as formula or also directly on the solver).

Depending on the type of cardinality constraint it uses the encoding algorithm as specified either in the optional given config or if it not present the one configured in the formula factory.

Returns an error if the input constraint cannot be converted to an incremental constraint which is the case if it is an exo-constraint, a tautology or contradiction, or a trivial constraint (all literals are set to true or false)

func (*CCIncrementalData) NewLowerBound 

func (cc *CCIncrementalData) NewLowerBound(rhs int) []f.Formula

NewLowerBound tightens the lower bound of an at-least-k constraint and returns the resulting formula.

Usage constraints:

  • New right-hand side must be greater than current right-hand side.
  • Cannot be used for at-most-k constraints.

func (*CCIncrementalData) NewLowerBoundForSolver 

func (cc *CCIncrementalData) NewLowerBoundForSolver(rhs int)

NewLowerBoundForSolver tightens the lower bound of an at-least-k constraint and encodes it on the solver of the result.

Usage constraints:

  • New right-hand side must be greater than current right-hand side.
  • Cannot be used for at-most-k constraints.

func (*CCIncrementalData) NewUpperBound 

func (cc *CCIncrementalData) NewUpperBound(rhs int) []f.Formula

NewUpperBound tightens the upper bound of an at-most-k constraint and returns the resulting formula.

Usage constraints:

  • New right-hand side must be smaller than current right-hand side.
  • Cannot be used for at-least-k constraints.

func (*CCIncrementalData) NewUpperBoundForSolver 

func (cc *CCIncrementalData) NewUpperBoundForSolver(rhs int)

NewUpperBoundForSolver tightens the upper bound of an at-most-k constraint and encodes it on the solver of the result.

Usage constraints:

  • New right-hand side must be smaller than current right-hand side.
  • Cannot be used for at-least-k constraints.

type Config 

type Config struct {
	AMOEncoder AMOEncoder
	AMKEncoder AMKEncoder
	ALKEncoder ALKEncoder
	EXKEncoder EXKEncoder
	PBCEncoder PBCEncoder

	BimanderGroupSize      BimanderGroupSize
	BimanderFixedGroupSize int
	NestingGroupSize       int
	ProductRecursiveBound  int
	CommanderGroupSize     int

	BinaryMergeUseGAC                bool
	BinaryMergeNoSupportForSingleBit bool
	BinaryMergeUseWatchDog           bool
}

Config describes the configuration for a cardinality or pseudo-Boolean encoding. This configuration struct defines the encoding algorithms for each type of constraint and their respective configuration parameters.

func DefaultConfig 

func DefaultConfig() *Config

DefaultConfig returns the default configuration for an encoder configuration.

func (Config) DefaultConfig 

func (Config) DefaultConfig() configuration.Config

DefaultConfig returns the default configuration for an encoder configuration.

func (Config) Sort 

func (Config) Sort() configuration.Sort

Sort returns the configuration sort (Encoder).

type EXKEncoder 

type EXKEncoder byte
const (
	EXKTotalizer EXKEncoder = iota
	EXKCardinalityNetwork
	EXKBest
)

CcExkEncoder represents the different algorithms for encoding an exactly-k constraint (EXK) to a CNF.

func (EXKEncoder) String 

func (i EXKEncoder) String() string

type FormulaEncoding 

type FormulaEncoding struct {
	// contains filtered or unexported fields
}

FormulaEncoding implements a Result backed by a formula factory. The resulting CNF is therefore stored as a list of clauses in the Result field.

func ResultForFormula 

func ResultForFormula(fac f.Factory) *FormulaEncoding

ResultForFormula creates a new encoding result backed by the given formula factory.

func (*FormulaEncoding) AddClause 

func (r *FormulaEncoding) AddClause(literals ...f.Literal)

AddClause adds a set of literals as a clause to the encoding result.

func (*FormulaEncoding) Factory 

func (r *FormulaEncoding) Factory() f.Factory

formula factory. Factory returns the backing formula factory from the encoding result.

func (*FormulaEncoding) Formulas 

func (r *FormulaEncoding) Formulas() []f.Formula

Formulas returns the encoding as a list of formulas.

func (*FormulaEncoding) NewAuxVar added in v0.3.0 

func (r *FormulaEncoding) NewAuxVar(sort f.AuxVarSort) f.Variable

NewAuxVar returns a new auxiliary variable of the given sort from the formula factory.

type PBCEncoder 

type PBCEncoder byte
const (
	PBCSWC PBCEncoder = iota
	PBCBinaryMerge
	PBCAdderNetworks
	PBCBest
)

PbcEncoder represents the different algorithms for encoding a pseudo-Boolean constraint to a CNF.

func (PBCEncoder) String 

func (i PBCEncoder) String() string

type Result 

type Result interface {
	AddClause(literals ...f.Literal)
	NewAuxVar(sort f.AuxVarSort) f.Variable
	Factory() f.Factory
	Formulas() []f.Formula
}

A Result is used to abstract CNF encodings for cardinality and pseudo-Boolean constraints. It provides methods for adding clauses, creating new auxiliary variables and accessing the result.

In LogicNG there are two implementations of this abstraction: one backed by a formula factory where the result is a list of clauses, and one backed by a SAT solver, where the clauses are added directly to the solver.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.