Tag: failed literal probing

  • CryptoMiniSat 5.6.3 Released

    The latest CryptoMiniSat, version 5.6.3 has been released. This release marks the 12’000th commit to this solver that has weathered more than I originally intended it to weather. It’s been an interesting ride, and I have a lot to thank Kuldeep and NSCC‘s ASPIRE-1 cluster for this release. I have burned over 200k CPU hours […]

  • Testing CryptoMiniSat using GoogleTest

    Lately, I have been working quite hard on writing module tests for CryptoMinisat using GoogleTest. I’d like to share what I’ve learnt and what surprised me most about this exercise. An example First of all, let me show how a typical test looks like: TEST_F(intree, fail_1) { s->add_clause_outer(str_to_cl(” 1, 2″)); s->add_clause_outer(str_to_cl(“-2, 3”)); s->add_clause_outer(str_to_cl(“-2, -3”)); inp->intree_probe(); check_zero_assigned_lits_contains(s, “-2”); […]

  • Failed literal probing and UIP

    I have just realised that CryptoMiniSat, having won a number of medals, does one of the most basic things, failed literal probing, all wrong. Let me tell you why it’s all wrong. In essence, failed literal probing is trivial. We enqueue a fact, such as a, and then propagate it. If this fails, i.e. if […]

  • CCC madness

    The Chaos Computer Club (CCC) is having its yearly conference starting today. It’s a madhouse here, which is great for ideas, so I have been having this rush of ideas implemented. First off, it seems that complex problems with few variables are way too difficult to solve even with distributed solving. I have been trying […]

  • On failed literal probing

    Apparently, there have been quite some work done on failed literal probing, although I don’t think they have all been put into a common package yet. The idea is quite simple in its purest form: try to set variable v1 to true and see if that fails. If it does, variable v1 must be false. […]