compute prime numbers up to number m

Make a nxn-bit matrix with variables names xij where x is given as argument

Make a n-bit vector with variables names xi where x is given as argument

This formula lists all directed graphs that have a triangle.

DirectStorageAccess: Interpret variables x as an address adr given as a binary number and select bit y[adr] of the vector y

This function computes the boolean formula that holds iff exactly k of the formulas in the given bitvector hold.

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.

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).

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

Generate the propositional formulas for the sum bits of the addition of the radix-2 numbers given as the arguments (as boolean variables).

Generate the propositional formula to check x

This function computes the circuit for radix-2 multiplication

Generate the propositional formulas for the sum bits of the subtraction of the radix-2 numbers given as the arguments (as boolean variables).

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.

generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a prime number as a radix-2 number

generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a square number as a radix-2 number

This function computes the threshold function, i.e., the generated formula holds iff k

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

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.

pigeonhole P N states that

compute propositional logic formula to state that N queens can be placed on a NxN board such that none can beat any other one.