Lògica a la Informàtica
Lab 2

  • Pràctica 1: SAT solver
    • How’s the performance of ./misat with the changes so far?
    • indexOfNextLitToPropagate
    • Heuristics for getNextDecisionLiteral()
  • Random k-CNFs
  • SAT solvers in practice

February 27, 2026

Typos en SAT-alumnes.cpp

  • Usually SAT-solvers return 10 when the CNF is SATISFIABLE and return 20 when it is not.
  • SAT-alumnes.cpp takes the opposite convention, this does not affect the code, but it is better to follow the convention
  • exchange all return 10 with return 20 in the SAT-alumnes.cpp

Do experiments with unsatisfiable instances (with 300 variables).

What is the role of indexOfNextLitToPropagate?

bool propagateGivesConflict ( ) {
  while ( indexOfNextLitToPropagate < modelStack.size() ) {
    // propagate only the literal in modelStack[indexOfNextLitToPropagate]
    ++indexOfNextLitToPropagate;
    for (uint i = 0; i < numClauses; ++i) {
      bool someLitTrue = false;
      int numUndefs = 0;
      int lastLitUndef = 0;
      for (uint k = 0; not someLitTrue and k < clauses[i].size(); ++k){
    int val = currentValueInModel(clauses[i][k]);
    if (val == TRUE) someLitTrue = true;
    else if (val == UNDEF){ ++numUndefs; lastLitUndef = clauses[i][k]; }
      }
      if (not someLitTrue and numUndefs == 0) return true; // conflict! all lits false
      else if (not someLitTrue and numUndefs == 1) setLiteralToTrue(lastLitUndef);  
    }    
  }
  return false;
}

indexOfNextLitToPropagate is a way to use modelStack also as a queue of the literals to propagate. It points at the beginning of the queue.

Unit propagation can be faster than kissat! why?

Possible heuristics for getNextDecisionLiteral()

  • for every variable x count
    • number N_x of occurrences (as positive and negative literal)
  • next literal to decide?
    • the undefined variable x with higher N_x
    • set it positively or negatively?
      it does not matter (in this type of algorithms of pure backtracking)
  • for every variable x count
    • number of positive occurrences N^+_x
    • number of negative occurrences N^-_x
  • next literal to decide?
    • the one with larger \min\{N^+_x,N^-_x\}
    • setting x positively and negatively has a chance to propagate a lot (with both polarities)
  • for every variable x count
    • how many times x appeared in a conflict:
      every time there is a conflict increment the counter for the variables in that clause
  • next literal to decide?
    • an undecided one that appeared in a lot of conflicts
  • for every variable x count
    • how many times x appeared in a recent conflict: To obtain this, divide all counters by 2 every R conflicts divide. Older conflicts are divided by 2 many times and will be less important.
      What value for R? This is a bit of experimental dark magic, try some values and see the effects.
  • next literal to decide?
    • an undecided one that appeared in a lot of recent conflicts

Random 3-SAT

\varphi\sim \mathcal{R}(n,m,k) is sampled according to the following process:

  • repeat m times:
    • begin the creation of a new clause
    • select S\subseteq \{x_1,\dots,x_n\} of size k uniformly at random;
    • for each variable x_i in S, independently, add \begin{cases}x_i & \text{with prob. }1/2\\\lnot x_i & \text{with prob. }1/2\end{cases} to the literals of the current clause

Is \varphi\sim \mathcal{R}(n,3,k) satisfiable?

Is \varphi\sim\mathcal{R}(n,n^2,k) satisfiable?

The satisfiability threshold for random k-SAT

Conjecture:
For every k\geq 2, there is a value \delta_k, s.t. for every \epsilon,

  • \lim_{n\to \infty}\mathrm{Pr}_{\varphi\sim\mathcal{R}(n,(\delta_k -\epsilon)n,k)}[\varphi \text{ is SAT}]=1
  • \lim_{n\to \infty}\mathrm{Pr}_{\varphi\sim\mathcal{R}(n,(\delta_k +\epsilon)n,k)}[\varphi \text{ is UNSAT}]=1

What is known

  • \delta_2=1 [CR92]
  • \delta_3\approx 4.26 (experimentally)
  • there is a k_0, s.t. for all k>k_0 the conjecture is true (2^k\ln 2-2\leq\delta_k\leq 2^k\ln 2). [DSS22]

Real state-of-the-art SAT solvers