rustsat-cadical 0.7.5

Interface to the SAT solver CaDiCaL for the RustSAT library.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

#include "internal.hpp"

namespace CaDiCaL {

// Sam Buss suggested to debug the case where a solver incorrectly claims
// the formula to be unsatisfiable by checking every learned clause to be
// satisfied by a satisfying assignment.  Thus the first inconsistent
// learned clause will be immediately flagged without the need to generate
// proof traces and perform forward proof checking.  The incorrectly derived
// clause will raise an abort signal and thus allows to debug the issue with
// a symbolic debugger immediately.

void External::check_solution_on_learned_clause () {
  assert (solution);
  for (const auto &lit : internal->clause)
    if (sol (internal->externalize (lit)) == lit)
      return;
  fatal_message_start ();
  fputs ("learned clause unsatisfied by solution:\n", stderr);
  for (const auto &lit : internal->clause)
    fprintf (stderr, "%d ", lit);
  fputc ('0', stderr);
  fatal_message_end ();
}

void External::check_solution_on_shrunken_clause (Clause *c) {
  assert (solution);
  for (const auto &lit : *c)
    if (sol (internal->externalize (lit)) == lit)
      return;
  fatal_message_start ();
  for (const auto &lit : *c)
    fprintf (stderr, "%d ", lit);
  fputc ('0', stderr);
  fatal_message_end ();
}

void External::check_no_solution_after_learning_empty_clause () {
  assert (solution);
  FATAL ("learned empty clause but got solution");
}

void External::check_solution_on_learned_unit_clause (int unit) {
  assert (solution);
  if (sol (internal->externalize (unit)) == unit)
    return;
  FATAL ("learned unit %d contradicts solution", unit);
}

} // namespace CaDiCaL