IMPORTANT: it came to our attention last week that a US patent published at the end of August 2008 was covering both the Watched Literals data structure used in modern SAT solvers and the VSIDS heuristics.
The heuristics used in SAT4J are derived from the one of Minisat and should not be affected by the patent. Regarding Watched Literals, we feel it is safer for us to move back to the Head/Tail data structure introduced in SATO from which is derived the WL data structure.
WE STRONGLY ENCOURAGE ALL USERS TO UPDATE TO THIS RELEASE.
IF YOU ARE USING SAT4J IN A COMMERCIAL TOOL, PLEASE NOTE THAT YOU MIGHT BE IN THE SCOPE OF A PATENT. CONTACT US FOR DETAILS.
Replaced the Watched Literals lazy data structure that is covered by a US patent (see SAT Live! for details) by the Head Tail data structure.
The resulting solvers are currently slower than the ones using the WL data structure (around a factor of 1.5). The code changes made should not be noticed by most of the users, i.e. should not have any consequence on their code.