BooleanFunctions (Averest)

BooleanFunctions Module

Namespace: Averest.TeachingTools
Assembly: Averest.dll

This module implements functions for generating some special boolean functions like arithmetic circuits for addition, subtraction, multiplication, threshold functions, the hidden weighted bit functions, the queen's problem, and the pigeonhole problems.

Functions and values

Function or value	Description
`ComputePrimeNumbers m` Full Usage: `ComputePrimeNumbers m` Parameters: m : `int` Returns: `Set<int>`	compute prime numbers up to number m m : `int` Returns: `Set<int>`
`MkBitmatrix x m n` Full Usage: `MkBitmatrix x m n` Parameters: x : `string` m : `int` n : `int` Returns: `BoolExpr[][]`	Make a nxn-bit matrix with variables names xij where x is given as argument x : `string` m : `int` n : `int` Returns: `BoolExpr[][]`
`MkBitvector x n` Full Usage: `MkBitvector x n` Parameters: x : `string` n : `int` Returns: `BoolExpr array`	Make a n-bit vector with variables names xi where x is given as argument x : `string` n : `int` Returns: `BoolExpr array`
`MkClique3 x` Full Usage: `MkClique3 x` Parameters: x : `BoolExpr[][]` Returns: `BoolExpr`	This formula lists all directed graphs that have a triangle. x : `BoolExpr[][]` Returns: `BoolExpr`
`MkDirectStorageAccess x y` Full Usage: `MkDirectStorageAccess x y` Parameters: x : `BoolExpr[]` y : `BoolExpr[]` Returns: `BoolExpr`	DirectStorageAccess: Interpret variables x as an address adr given as a binary number and select bit y[adr] of the vector y x : `BoolExpr[]` y : `BoolExpr[]` Returns: `BoolExpr`
`MkExactlyKofN k x` Full Usage: `MkExactlyKofN k x` Parameters: k : `int` x : `BoolExpr array` Returns: `BoolExpr`	This function computes the boolean formula that holds iff exactly k of the formulas in the given bitvector hold. k : `int` x : `BoolExpr array` Returns: `BoolExpr`
`MkHiddenWeightedBit n` Full Usage: `MkHiddenWeightedBit n` Parameters: n : `int` Returns: `BoolExpr`	This function computes the hidden weighted bit function which has only exponentially sized BDDs. It is the disjunction of all formulas x[k] & (MkExactlyKofN (k+1) x) for k in [0..n-1] where n is the length of x, and moreover at least one of the x[i] must hold. n : `int` Returns: `BoolExpr`
`MkListNatAdd x` Full Usage: `MkListNatAdd x` Parameters: x : `BoolExpr[][]` Returns: `BoolExpr[]`	Generate the propositional formulas for the sum bits of the addition of m different n-bit radix-2 numbers (given as rows of a matrix x). x : `BoolExpr[][]` Returns: `BoolExpr[]`
`MkMultiples k x` Full Usage: `MkMultiples k x` Parameters: k : `int` x : `BoolExpr[]` Returns: `BoolExpr`	generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a multiple of k as a radix-2 number k : `int` x : `BoolExpr[]` Returns: `BoolExpr`
`MkNatAdd x y` Full Usage: `MkNatAdd x y` Parameters: x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr array`	Generate the propositional formulas for the sum bits of the addition of the radix-2 numbers given as the arguments (as boolean variables). x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr array`
`MkNatLes x y` Full Usage: `MkNatLes x y` Parameters: x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr`	Generate the propositional formula to check x x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr`
`MkNatMul x y` Full Usage: `MkNatMul x y` Parameters: x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr[]`	This function computes the circuit for radix-2 multiplication x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr[]`
`MkNatSub x y` Full Usage: `MkNatSub x y` Parameters: x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr array`	Generate the propositional formulas for the sum bits of the subtraction of the radix-2 numbers given as the arguments (as boolean variables). x : `BoolExpr array` y : `BoolExpr array` Returns: `BoolExpr array`
`MkPopulationCount x` Full Usage: `MkPopulationCount x` Parameters: x : `BoolExpr array` Returns: `BoolExpr array`	This function computes the population count, i.e., the number of bits that are true as radix-2 number with the minimal number of bits. x : `BoolExpr array` Returns: `BoolExpr array`
`MkPrime x` Full Usage: `MkPrime x` Parameters: x : `BoolExpr[]` Returns: `BoolExpr`	generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a prime number as a radix-2 number x : `BoolExpr[]` Returns: `BoolExpr`
`MkSquares x` Full Usage: `MkSquares x` Parameters: x : `BoolExpr[]` Returns: `BoolExpr`	generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a square number as a radix-2 number x : `BoolExpr[]` Returns: `BoolExpr`
`MkThresholdMoreThanK k x` Full Usage: `MkThresholdMoreThanK k x` Parameters: k : `int` x : `BoolExpr array` Returns: `BoolExpr`	This function computes the threshold function, i.e., the generated formula holds iff k k : `int` x : `BoolExpr array` Returns: `BoolExpr`
`NatSetToBoolExpr x s` Full Usage: `NatSetToBoolExpr x s` Parameters: x : `BoolExpr[]` s : `Set<int>` Returns: `BoolExpr`	convert numbers in set s to a boolean expression assuming that all elements can be represented as radix-2 number with the bits from x x : `BoolExpr[]` s : `Set<int>` Returns: `BoolExpr`
`ZeroExtend x n` Full Usage: `ZeroExtend x n` Parameters: x : `BoolExpr array` n : `int` Returns: `BoolExpr array`	ZeroExtend adds n false bits as most significant bits to extend the length of a bitvector without changing its value as a radix-2 number. x : `BoolExpr array` n : `int` Returns: `BoolExpr array`
`pigeonhole N` Full Usage: `pigeonhole N` Parameters: N : `int` Returns: `BoolExpr`	pigeonhole P N states that N : `int` Returns: `BoolExpr`
`queen N` Full Usage: `queen N` Parameters: N : `int` Returns: `BoolExpr`	compute propositional logic formula to state that N queens can be placed on a NxN board such that none can beat any other one. N : `int` Returns: `BoolExpr`