general.hpp File Reference

Plans regarding pseudo-boolean constraints. More...

Go to the source code of this file.

Detailed Description

Plans regarding pseudo-boolean constraints.

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 Maxima-matrix.
  • One had then to sort the rows of A, x accordingly, which seems alright.
  • A special case is an xor-constraint x_1 + ... + x_n = b with b in {0,1} (if b is a literal, then it can be moved to the left-hand 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.