Documentation
¶
Overview ¶
Package assignment provides a data structure for Boolean assignments in LogicNG, mapping Boolean variables to truth values.
In contrast to the model found in the [model] package, an assignment stores the variables internally in such a way that it can be efficiently used for evaluation and restriction.
The primary use case for assignments is their usage in the functions Evaluate and Restrict.
The following example creates an assignment and restricts and evaluates a formula with it.
fac := formula.NewFactory()
formula := fac.And(fac.Variable("a"), fac.Variable("b")) // formula a & b
ass := assignment.New(fac, fac.Variable("a")) // assigns a to true
eval := Evaluate(fac, formula, ass) // evaluates to false (b is false)
restrict := Restrict(fac, formula, ass) // restricts to b
Index ¶
- func Evaluate(fac f.Factory, formula f.Formula, assignment *Assignment) bool
- func EvaluatesToFalse(fac f.Factory, formula f.Formula, assignment map[f.Variable]bool) bool
- func EvaluatesToTrue(fac f.Factory, formula f.Formula, assignment map[f.Variable]bool) bool
- func Restrict(fac f.Factory, formula f.Formula, assignment *Assignment) f.Formula
- type Assignment
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Evaluate ¶
Evaluate evaluates the formula with the given assignment. A literal not covered by the assignment evaluates to false if it is positive and true if it is negative.
func EvaluatesToFalse ¶
EvaluatesToFalse reports whether the formula evaluates to false under the assignment (mapping from variables to truth values).
If a partial assignment is given, the check only recognizes simple unsatisfiable/tautology cases
- operand of an AND/OR is false/true
- all operators of an OR/AND are false/true
- AND/OR has two operands with complementary negations
This evaluation differs from the standard Evaluate in two ways:
- It accepts partial assignments
- It tries to avoid the generation of intermediate formulas to speed up the performance
func EvaluatesToTrue ¶
EvaluatesToTrue reports whether the formula evaluates to true under the assignment (mapping from variables to truth values).
If a partial assignment is given, the check only recognizes simple unsatisfiable/tautology cases
- operand of an AND/OR is false/true
- all operators of an OR/AND are false/true
- AND/OR has two operands with complementary negations
This evaluation differs from the standard Evaluate in two ways:
- It accepts partial assignments
- It tries to avoid the generation of intermediate formulas to speed up the performance
Types ¶
type Assignment ¶
type Assignment struct {
// contains filtered or unexported fields
}
An Assignment represents a mapping from Boolean variables to truth values
func New ¶
New creates a new Assignment with the given literals. Literals with a positive phase are added as a mapping to true, literals with a negative phase as a mapping to false. Returns an error, if the literals list contains complementary literals.
func (*Assignment) AddLit ¶
AddLit add a single literal to the assignment. A literal with a positive phase is added as a mapping to true, a literal with a negative phase as a mapping to false.
func (*Assignment) NegVars ¶
func (a *Assignment) NegVars() []f.Variable
NegVars returns all variables of the assignment mapped to false. Note, this function return the variables, not the negative literals.
func (*Assignment) PosVars ¶
func (a *Assignment) PosVars() []f.Variable
PosVars returns all variables of the assignment mapped to true.
func (*Assignment) Size ¶
func (a *Assignment) Size() int
Size returns the number of variables in the Assignment.
Source Files