Plans regarding pseudoboolean constraints.
More...
Go to the source code of this file.
Detailed Description
Plans regarding pseudoboolean constraints.
 Todo:
 Connections
 Todo:
 The notion of a "linear constraint"

Update needed; see Satisfiability/Lisp/Generators/LinearEquations.mac.

Consider an mxn matrix A of ZZ_2 and two vectors x, b of length n, with entries either literals or from ZZ_2 (the latter not for x).

The condition to be modelled is "A * x = b".

Likely for the specification of x, b one must explicitly distinguish between values 0, 1 and literals, since 1 can be a variable, and 1 is a literal, but could also be interpreted as +1 in ZZ_2.

Complementation of literals is also to be distinguished from negation in ZZ_2.

This could be represented as a list [A,x,[b1,b2]], where b1 contains the constant parts of b, while b2 contains the literals. x as well as b1,b2 are lists, while A is a Maximamatrix.

One had then to sort the rows of A, x accordingly, which seems alright.

A special case is an xorconstraint x_1 + ... + x_n = b with b in {0,1} (if b is a literal, then it can be moved to the lefthand side).

This can be represented as a list [x, b], where x is a list of literals, and b in {0,1}.

For discussions on the notion of constraint, see 'Notion of "constraint"' in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/plans/Translations.hpp.
Definition in file general.hpp.