Propositional Logic – syntax

X set of propositional variables (e.g., p, q, r, etc.)

F is a propositional formula (over the set of variables X) if
it is built from the variables in X and logical connectives

• \land (AND)
• \lor (OR)
• \lnot (NOT)

• Is p\land (q \lor \lnot r) a propositional formula?
• Is p\to q a propositional formula?
• Is p\land q\land \lnot r a propositional formula?

Conjunctive Normal Form (CNF)

A propositional formula F is a CNF, if

• F=C_1\land C_2\land \dots\land C_m for some m and
• each C_i is a disjunction of variables or negated variables

Propositional Logic – semantics

Any function I: X \to \{0, 1\} is an interpretation.
1 means true, and 0 means false.

Satisfiability – terminology

I: X \to \{0, 1\} interpretation
F propositional formula

SAT / CNF-SAT / k-SAT

SAT
Input: a propositional formula F
Output: Yes/No, Yes if F is satisfiable.

Encodings

Sudoku, graph coloring, and many other combinatorial problems can be encoded as CNF-SAT problems.

How could you encode Sudoku as a CNF-SAT problem?

Generic plan

In this course we will:

• choose an arbitrary problem P (e.g., Sudoku, graph coloring, etc.)
• encode it as a CNF formula F_P
• give the formula F_P as input to a SAT-solver in the .cnf DIMACS CNF format
• call a SAT solver with the .cnf file as input
• recover a solution of P (if any) from the model that the SAT solver gives us (if any)
  

Pràctica 1 – SAT solver

This first practical assignment has the following objectives:

• to confront an NP-complete problem, namely SAT
• to gain foundational knowledge of SAT solvers

To achieve this, you will need to improve the efficiency of a SAT solver that is provided to you.

https://www.cs.upc.edu/~li/practica1.html

Deadline: 08/03/2026 23:59
SAT-alumnes.cpp, i temps.txt with the output of the script

DIMACS CNF file format

c Lines starting with 'c' are comments 
c N is the number of variables, M is the number of clauses
p cnf N M
clause1 0
clause2 0
...
clauseM 0

Each clause is a sequence of integers ending with 0:
k represents the literal x_k
-k represents the literal \lnot x_k

c  simple example
c what is the CNF formula represented by this DIMACS CNF file?
c Is it satisfiable? 
p cnf 3 2
1 -3 0
2 3 -1 0

Algorithms to solve CNF-SAT

SAT-alumnes.cpp

• Download the file SAT-alumnes.cpp from the course webpage, the Makefile and compile with make.
• test misat on some simple .cnf example.

All set?

Kissat

Install Kissat, unless it is already installed on your system.
Kissat is a state-of-the-art CDCL SAT solver.

Benchmark we will use

You’ll test your SAT-solver on random 3-CNFs with up to 300 variables
i.e., formulas in CNF where each clause has exactly 3 literals generated by the following random process:

• fix the number of variables n and the number of clauses m
• for each clause, select 3 distinct variables uniformly at random from the n variables
• for each selected variable, decide uniformly at random whether to include it as a positive or negative literal in the clause

Extra: CNFgen

CNFgen produces benchmark propositional formulas in DIMACS format, ready to be fed to SAT solvers. Many of these formulas encode structured combinatorial problems well known to be challenging for certain SAT solvers.

pip3 install [--user] cnfgen

for example cnfgen php 10 7 gives the Pigeonhole Principle from 10 pigeons and 7 holes.

Let’s look into SAT-alumnes.cpp

int main(){ 
  readClauses(); // reads numVars, numClauses and clauses
  model.resize(numVars+1,UNDEF);
  indexOfNextLitToPropagate = 0;  
  decisionLevel = 0;
  
  // Take care of initial unit clauses, if any
  for (uint i = 0; i < numClauses; ++i)
    if (clauses[i].size() == 1) {
      int lit = clauses[i][0];
      int val = currentValueInModel(lit);
      if (val == FALSE) {cout << "UNSATISFIABLE" << endl; return 10;}
      else if (val == UNDEF) setLiteralToTrue(lit);
    }
  
  // DPLL algorithm
  while (true) {
    while ( propagateGivesConflict() ) { #<1>
      if ( decisionLevel == 0) { cout << "UNSATISFIABLE" << endl; return 10; }
      backtrack();
    }
    int decisionLit = getNextDecisionLiteral();
    if (decisionLit == 0) { checkmodel(); cout << "SATISFIABLE" << endl; return 20; }
    // start new decision level:
    modelStack.push_back(0);  // push mark indicating new DL
    ++indexOfNextLitToPropagate;
    ++decisionLevel;
    setLiteralToTrue(decisionLit);    // now push decisionLit on top of the mark
  }
}  

1. The propagateGivesConflict() function unit propagates until it is no longer possible, and returns true if a conflict is found, i.e., if some clause is falsified by the current model.

How to work on this practice assignment?

• Study in detail how the provided SAT solver works, and understand the code.
• Follow the instructions on the page https://www.cs.upc.edu/~li/practica1.html
• More concretely, you need to
  • speed up the propagateGivesConflict()
  • give a less naïve heuristic for getNextDecisionLiteral()

propagateGivesConflict()

bool propagateGivesConflict ( ) {
  while ( indexOfNextLitToPropagate < modelStack.size() ) {
    ++indexOfNextLitToPropagate;
    for (uint i = 0; i < numClauses; ++i) { # <1>
      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;
}

1. Instead of iterating over all clause use OccurLists to keep track of the clauses relevant to the current propagation step.

getNextDecisionLiteral()

// Heuristic for finding the next decision literal:
int getNextDecisionLiteral(){
  for (uint i = 1; i <= numVars; ++i) // stupid heuristic: #<1>
    if (model[i] == UNDEF) return i;  // returns first UNDEF var, positively
  return 0; // reurns 0 when all literals are defined
}

1. Instead of taking the first undefined variable use a variable with impact.

Next lab (tentative)

• real world usage of SAT-solvers
  • certificates of correctness
  • SAT competition
• more on random k-CNF
  • phase transition
• More on the heuristics for SAT-alumnes.cpp