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 (including SAT4J) 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.