Symmetry Breaking vs NbModels

[Bart Bogaerts]

When using symmetry breaking, we do not return all models; the options of symmetry breaking and nbmodels are therefore inconsistent.

We should either * Give the user the possibility to choose whether or not he wants all models (and generate them by postprocessing) * * Thus: Make the symmetry breaking option: Static-AllModels / Static-LessModels / SPFS-AllModels / SPFS-LessModels * Or, by default return less models, but make an inference that allows to calculate the rest

This should be well-documented.

[JoD]

When calculating all clauses, you probably need an efficient method to check whether a certain clause/solution already exists in a collection of clauses/solutions. One approach would be based on a bit representation of a clause, with for each variable a bit whether the variable is in the clause, and a bit whether the variable is a positive or negative lit. This bit representation can be transformed to a series of unsigned integer hash values, depending on the integer bit size (typically 64 or 32) of the hardware.

For instance: 10 variables range a-j, bit size 4 (so unsigned int range 0-15). Clause (a, ~d, ~j) will have the following 6 integer hash values: variables: 1001 0000 0100 signs: 0001 0000 0100 => as integers: 9 0 2 8 0 2.

Now make a recursive hash map of a set of clauses using the above hashes, and you're set.

[Broes De Cat]

Refs #164 #90, fixes #163 fixes #115

Printers also use checkTermination. Derivetermbounds throws an internal exception whenever no bounds could be derived. Several types should still be handled. Symmetrybreaking throws a warning when multiple models are requested. Symmetrybreaking + optimization now throws.

→ 7a018a91f28d

[JoD]

This will be fixed together with implementing the symmetry propagation routines in MinisatID.

[Broes De Cat]

Removing milestone: Later (automated comment)