Tag: bug
-
On variable renumbering
Variable renumbering in SAT solvers keeps a mapping between the external variable numbers that is visible to the users and the internal variable numbers that is visible the to the system. The trivial mapping that most SAT solvers use is the one-to-one mapping where there is no difference between outer and internal variables. A smart […]
-
My SAT solver fuzzing setup
Since the SAT solver fuzzing paper by Brummayer, Lonsing and Biere, SAT solver fuzzing has been quite the thing in the SAT community. Many bugs have since been discovered in almost all SAT solvers, including those of this author. In this blog post I will detail my SAT fuzzing setup: what fuzzers I use and […]
-
CryptoMiniSat 3.3 released
This is just a short note that CryptoMiniSat 3.3 has been released. This is mainly a bugfix release. I have managed to make a fuzzer that simulates library usage of the system by interspersing the CNF with “c Solver::solve()” calls and then checking the intermediate solutions. Checking is either performed by verifying that all clauses […]
-
GCC 4.5.2 at the SAT Competition’13
(Note update below) Just a short note. All MiniSat-derived SAT solvers might give wrong results during the competition. No, MiniSat doesn’t have a bug. GCC has a giant bug. Vegard reported this years ago — I personally put about 12h tracking it down, posted it to the CryptoMiniSat mailing list, and Vegard took it up, […]
-
Q-DIMM, an “innovation” by ASUS
Lately, I have been having boot problems with my computer: the system would sometimes fail to boot, and at other times, it displayed the wrong memory readings. I was puzzled, so I took a look. I have six memory DIMMs installed in an ASUS motherboard. Memory modules are usually retained in their slots using two […]