Propositional Logic Proof System

Revisit the definitions:

A literal is either an atomic proposition $p$ or its negation $\neg p$
A clause is a disjunction of literals
- e.g., $p \vee \neg q \vee r$
A formula is in Conjunctive Normal Form (CNF) if it is a conjunction of disjunctions of literals (i.e., a conjunction of clauses): $\bigwedge_{i=1}^n\left(\bigvee_{j=1}^{m_i} L_{i, j}\right)$ $⋀_{i = 1}^{n} (⋁_{j = 1}^{m_{i}} L_{i, j})$
- e.g., $(p \vee \neg q) \wedge(r \vee q)$

A formula is in Disjunctive Normal Form (DNF) if it is a disjunction of conjunctions of literals: $\bigvee_{i=1}^n\left(\bigwedge_{j=1}^{m_i} L_{i, j}\right)$

Formula and Satisfiability

A formula $F$ is satisfiable if and only if $F$ has a model (i.e. it can be 1), otherwise $F$ is unsatisfiable (or contradictory)

DNF and Satisfiability

If the formula is in DNF, it is easy to determine satisfiability.
- formula is satisfied if any clause in the formula is satisfied

CNF and Satisfiability

Unlike DNF, it is not easy to determine satisfiability.

But almost all SAT solvers first convert formula to CNF before solving

Interesting Question: If it is just as expensive to convert formula to CNF as to DNF, why do solvers convert to CNF although it is much easier to determine satisfiability in DNF?

Two reasons:

Possible to convert to equisatisfiable (not equivalent) CNF formula with only linear increase in size!

CNF makes it possible to perform interesting deductions (resolution)

Equisatisfiability

Two formulas $F$ $F$ and $F'$ $F^{'}$ are equisatisfiable if and only if:
- $F$ is satisfiable if and only if $F'$ is satisfiable

Finding satisfiability of $F$

To determine satisfiability of $F$ , convert formula to equisatisfiable formula $F'$ in CNF

Then use an algorithm (DPLL) to decide satisfiability of $F'$

Since $F'$ is equisatisfiable to $F$ , $F$ is satifiable if and only if algorithm decides $F'$ is satisfiable

How to convert formula to equisatisfiable formula without causing exponential blow-up in size?

Tesitin’s Transformation

Convert Formula $F$ into Equisat CNF Formula $F'$ in CNF with only a linear increase in size.

Example:

The size of resulting formula is bound by $30n + 2$ where $n$ is size of original formula.

Proof system

Proof System is a finite set of proof rules applied to logical formulas to achieve new statements.

Two important attributes of a proof system:

Soundness: every true statement proven by the proof system is indeed true in the logic
Completeness: every true statement in the logic can be proven by the proof system

Proof rule: A simple syntactic transformation applied to formulas

Resolution

Propositional resolution is a exponential proof principle for propositional logic.

Soundness
Completeness
There is only one proof rule: resolution
The goal: prove unsatisfiability of a formula

A general precondition for resolution: the formula (or set of formulas) is in CNF

Instead of using $F = (L_{1,1} \vee \cdots \vee L_{1, n_1}) \wedge \cdots \wedge (L_{k,1} \vee \cdots \vee L_{k, n_k})$

We use $F = (\{L_{1,1}, \cdots L_{1,n_1}\}, \cdots , \{L_{k,1}, \cdots L_{k,n_k}\})$

Simplifications stemming from associativity, commutativity, or idempotency are automatically provided by the set notation
Simpler understanding of the formula (using diagrams)
Simpler encoding of a problem to CNF

Compactness Theorem

Recall that a set $M$ of formulas is, by definition, satisfiable if there is an assignment $\mathcal{A}$ such that for every $F \in M$ , . $\mathcal{A}(F) = 1$ . We call such an assignment a model for $M$ .

A set M of formulas is satisfiable, if and only if, every finite subset of M is satisfiable

Propositional Resolution

$Res(\{C, p\}, \{D, \neg p\}) = \{C, D\}$

$\frac{C \vee p \quad D \vee \neg p}{R = C \vee D}$

where

$C \vee p, D \vee \neg p$ are the Pivot (literal)
$Res$ is the Resolvent

Resolution Lemma

Let $F$ be a CNF formula. Let $R$ be a resolvent of two clauses $C_1$ and $C_2$ in $F$ .

Then, $F \cup \{R\}$ is equivalent to $F$

Example:

$F = (\{A, B\}, \{\neg A, C\})$ is equivalent to $(\{A, B\}, \{\neg A, C\}, \{B, C\})$

Resolution Theorem

Let $F$ be a set of clauses, and consider the following definitions

$Res(F) = F \cup \{R | R \text{ is a resolvent of two clauses in } F \}$

$Res^0(F) = F$

$Res^{n+1}(F) = Res(Res^n(F)), \text{for }n \ge 0$

$Res^*(F) = \bigcup_{n \ge 0} Res^n(F)$

Resolution Theorem: A clause set $F$ is unsatisfiable if and only if $\square \in Res^*(F)$

Resolution Theorem Example

For the following set of clauses determine $Res^n(F)$ for $n = 0, 1, 2$

$F = (\{A, \neg B, C\}, \{B, C\}, \{\neg A, C\}, \{B, \neg C\}, \{\neg C\})$

n = 0:

$Res^0(F) = F = (\{A, \neg B, C\}, \{B, C\}, \{\neg A, C\}, \{B, \neg C\}, \{\neg C\})$

n = 1:

resolvent of $\{A, \neg B, C\}$ and $\{B, C\}$ = $\{A, C\}$
$Res^1(F) = F \cup \{A, C\} = (\{A, \neg B, C\}, \{B, C\}, \{\neg A, C\}, \{B, \neg C\}, \{\neg C\}, \{A, C\})$

n = 2:

resolvent of $\{A, \neg B, C\}$ and $\{\neg A, C\}$ = $\{\neg B, C\}$
$Res^2(F) = F \cup (\{A, C\}, \{\neg B, C\}) = (\{A, \neg B, C\}, \{B, C\}, \{\neg A, C\}, \{B, \neg C\}, \{\neg C\}, \{A, C\}, \{\neg B, C\})$

Resolution Theorem Example

Show that $F = (\{A,B,\neg C\}, \{\neg A\}, \{A, B, C\}, \{A, \neg B\})$ is unsatisfiable.

$C_1 = \{A,B,\neg C\}$ (clause in $F$ )
$C_2 = \{A, B, C\}$ (clause in $F$ )
$C_3 = \{A, B\}$ (resolvent of $C_1$ and $C_2$ )
$C_4 = \{A, \neg B\}$ (clause in $F$ )
$C_5 = \{A\}$ (resolvent of $C_3$ and $C_4$ )
$C_6 = \{\neg A\}$ (clause in $F$ )
$C_7 = \square$ (resolvent of $C_5$ and $C_6$ )

By definition, the empty clause $\square$ is unsatisfiable. Therefore, a clause set which contains $\square$ as an element is unsatisfiable. So $F$ is unsatisfiable.

Alternatively, we can use a Resolution Graph to show that $F = (\{A,B,\neg C\}, \{\neg A\}, \{A, B, C\}, \{A, \neg B\})$ is unsatisfiable.

Proof of Resolution theorem

using the compactness theorem, that is, a (possibly infinite) set M of propositional formulas is satisfiable if and only if every finite subset of M is satisfiable. We assume F is finite:

The empty clause is denoted by $\square$

Soundness: showing that $\square \in Res^*(F)$ implies that F is UNSAT.

use resolution lemma to show that F is equivalent to $Res^n(F)$ for any $n >= 0$
since $\square \in Res^*(F)$
then it is contained in $Res^{n+1}(F)$ for some $n$
Therefore, there are two clauses $\{L\} \{\neg L\}$ in $Res^n{(F)}$ .
$Res^{n}(F)$ is UNSAT

Completeness: showing that F is UNSAT implies $\square \in Res^*(F)$

proof by induction on n.
Base induction : n=0, therefore, $F = \{\text{square block}\}$ , therefore, $\square \in Res^*(F)$
Induction step: Let $F$ be a clause set with atomic formulas $A_1, A_2, ... , A_{n+1}$ (no clause has $A_{n+1}$ and $\neg A_{n+1}$ )
obtain $F_{0}$ and $F_1$ as follows: $F_0$ assigns $A_{n+1}$ to 0 (false), $F_1$ assigns $A_{n+1}$ to 1 (true)
We can show that both $F_0$ and $F_1$ are UNSAT (o.w F would be SAT too)
A sequence of clauses $C_1, C_2, ... , C_m$ exists for $F_0$ (similarly $C'_1, C'_2, ... , C'_m$ For $F_1$ ) that $C_m = \text{square block}$
Restoring $A_{n+1}$ in $F_0$ with $C_i$ , and carring $A_{n+1}$ in the resolution steps $\rightarrow$ $A_{n+1} \in Res^*(F)$
$A_{n+1}$ in $F_1$ with $C'_1$ and $\neg A_{n+1}$ $\rightarrow \neg A_{n+1} \in Res^*(F)$
Another resolution step $\rightarrow \square \in Res^*(F)$

SAT Solvers

Approaches

Naïve approach
- Enumerate truth table
DP:
- Approach derived directly from the proof of the resolution theorem
DPLL (Davis-Putnam-Logemman-Loveland) $\rightarrow$ $\to$ Basis of all modern SAT solvers
- Smart enumeration of all possible SAT assignments
CDCL
- Extends DPLL with Conflict-Driven-Clause-Learning

Minisat

MiniSat is one of the most famous modern SAT-solvers.

written in C++

designed to be easily understandable and customizable

many new SAT-solvers use MiniSAT as their base

Example of miniSAT

// defined std::unique_ptr
#include <memory>
// defines Var and Lit
#include "minisat/core/SolverTypes.h"
// defines Solver
#include "minisat/core/Solver.h"

#include <iostream>

int main(void){
  // create a new MiniSat solver object using a unique_ptr smart pointer
  std::unique_ptr<Minisat::Solver> solver(new Minisat::Solver());

  // declare an array of 12 Boolean literals and assign them to new variables in the solver
  Minisat::Lit x[12];
  for(int i=0; i<12; i++) x[i] = Minisat::mkLit(solver->newVar());

  // add three clauses to the solver representing constraints that must be satisfied to solve the SAT problem
  solver->addClause(x[0], x[3]); // x[0] or x[3]
  solver->addClause(x[0], ~x[2]); // x[0] or not x[2]
  solver->addClause(x[0], x[7], x[11]); // x[0] or x[7] or x[11]

  // call the solver's solve() method to try to find a satisfying assignment for the instance
  bool res = solver->solve();

  // print the result of the solver's solve() method
  std::cout << "The result is " << res << "\n";

  // if a satisfying assignment was found, print it
  if(res){
    std::cout << "Satisfying assignment is: ";
    for(int i=0; i<12; i++){
      std::cout << "x" << i << "=" << Minisat::toInt(solver->modelValue(x[i])) << " ";
    }
    std::cout << "\n";
  }

  return 0; // indicate successful completion
}

Note Minisat::toInt(solver->modelValue(l1)) == 1 means false, while 0 means true.

1 2	The result is 1 satisfying assignment is: x0=1 x1=1 x2=1 x3=0 x4=1 x5=1 x6=1 x7=0 x8=1 x9=1 x10=1 x11=1

c this is a comment
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

This is a CNF file, which represents a Boolean formula in conjunctive normal form. Here’s an explanation of each line:

“c this is a comment”: This line is a comment and is ignored by the solver. Comments start with the letter “c” and are used to provide information about the file.

“p cnf 5 3”: This line specifies that the formula is in CNF, has 5 variables, and contains 3 clauses.

“1 -5 4 0”: This line represents the first clause. It is a disjunction (OR) of three literals: variable 1, the negation of variable 5, and variable 4. The “0” at the end represents the end of the clause.

“-1 5 3 4 0”: This line represents the second clause. It is a disjunction of four literals: the negation of variable 1, variable 5, variable 3, and variable 4. Again, the “0” at the end represents the end of the clause.

“-3 -4 0”: This line represents the third clause. It is a disjunction of two literals: the negation of variable 3 and the negation of variable 4. The “0” at the end represents the end of the clause.

Overall, this formula represents a set of constraints on the five variables such that the formula is satisfied if and only if at least one of the three clauses is satisfied. The solver would try to find an assignment of truth values to the variables that satisfies all of the clauses, or report that the formula is unsatisfiable if no such assignment exists.

Example of miniSAT

// defined std::unique_ptr
#include <memory>
// defines Var and Lit
#include "minisat/core/SolverTypes.h"
// defines Solver
#include "minisat/core/Solver.h"

// defined std::cout
#include <iostream>

int main(void) {
    // -- allocate on the heap so that we can reset later if needed
    std::unique_ptr<Minisat::Solver> solver(new Minisat::Solver()); // create a new instance of MiniSAT solver and store a pointer to it in a unique_ptr

    // create four positive literals over four new variables
    Minisat::Lit l1, l2, l3, l4;
    l1 = Minisat::mkLit(solver->newVar());
    l2 = Minisat::mkLit(solver->newVar());
    l3 = Minisat::mkLit(solver->newVar());
    l4 = Minisat::mkLit(solver->newVar());

    // create three positive literals over three new variables
    Minisat::Lit b0, b1, b2;
    b0 = Minisat::mkLit(solver->newVar());
    b1 = Minisat::mkLit(solver->newVar());
    b2 = Minisat::mkLit(solver->newVar());

    // add clauses to the solver using the created literals to specify the disjunctive terms of each clause
    // (l1 || b0)
    solver->addClause(l1, b0);
    // (!b0 || l2 || b1)
    solver->addClause(~b0, l2, b1);
    // (!b1 || l3 || b2)
    solver->addClause(~b1, l3, b2);
    // (!b2|| l4)
    solver->addClause(~b2, l4);

    // call the solve method of the solver to solve the CNF formula represented by the added clauses
    bool res = solver->solve();

    // print the result of the solve method and the satisfying assignment that was found by the solver
    std::cout << "The result is: " << res << "\n";
    std::cout << "Satisfying assignment is: "
              << "l1=" << Minisat::toInt(solver->modelValue(l1)) << " "
              << "l2=" << Minisat::toInt(solver->modelValue(l2)) << " "
              << "l3=" << Minisat::toInt(solver->modelValue(l3)) << " "
              << "l4=" << Minisat::toInt(solver->modelValue(l4)) << " "
              << "b0=" << Minisat::toInt(solver->modelValue(b0)) << " "
              << "b1=" << Minisat::toInt(solver->modelValue(b1)) << " "
              << "b2=" << Minisat::toInt(solver->modelValue(b2)) << std::endl;

    // add more clauses to the solver
    std::cout << "Adding more clauses...\n";
    solver->addClause (~l1);
    solver->addClause (~l2);
    solver->addClause (~l3);
    solver->addClause (~l4);

    // check whether the CNF in the solver is still satisfiable
    res = solver->solve();

    // print the result of the solve method after adding more clauses
    std::cout << "New result is: " << res << "\n";

    // the next line de-allocates existing solver and allocates a new
    // one in its place.
    solver.reset (new Minisat::Solver());

    // at this point the solver is ready. You must create new
    // variable and new clauses
    return 0;
}

Output:

Note Minisat::toInt(solver->modelValue(l1)) == 1 means false, while 0 means true.

The result is: 1 
satisfying assignment is: l1=1 l2=0 l3=1 l4=1 b0=0 b1=1 b2=1
Adding more clauses...
New result is: 0

Practical Example of Using minisat to solve vertex cover problem:

std::vector<int> FindVertexCover(UndirectedGraph& graph, int k)
{
    // -- allocate on the heap so that we can reset later if needed
    std::unique_ptr<Minisat::Solver> solver(new Minisat::Solver()); // create a new instance of MiniSAT solver
    
    // Get number of vertex
    int n = graph.GetSize();
    // Get Edge for reduction
    std::vector<Edge> edgeList = graph.GetEdgeList();
    // Holding the result
    std::vector<int> cover;

    //The reduction uses n × k atomic propositions
    // declare an 2D array of n x k Boolean literals and assign them to new variables in the solver
	Minisat::Lit propositions[n][k];
    for (int v = 0; v < n; v++) 
    {
		for (int l = 0; l < k; l++) 
        {
            // Assign new variables to n × k atomic propositions
			propositions[v][l] = Minisat::mkLit(solver->newVar());
		}
	}

    //The reduction consists of the following clauses:
    //================================================================================
    //clauses1: At least one vertex is the ith vertex in the vertex cover:
    // ∀i ∈ [1,k], a clause(x_{1,i} ∨ x_{2,i} ∨···∨ x_{n,i})
	for (int i = 0; i < k; i++) // ∀i ∈ [1,k]
    {
        //See Vec.h in Minisat, Automatically resizable arrays (basically vector)
		Minisat::vec<Minisat::Lit> clauses;
		for (int v = 0; v < n; v++) 
        {
            Minisat::Lit x_vi = propositions[v][i];
			clauses.push(x_vi);
		}
        // (x_{1,i} || x_{2,i} ||···|| x_{n,i})
		solver->addClause(clauses);
	}

    //clauses2: No one vertex can appear twice in a vertex cover.
    // ∀m ∈ [1, n], ∀p,q ∈ [1, k] with p < q, a clause (¬x_{m,p} ∨ ¬x_{m,q})
    // In other words, it is not the case that vertex m appears both in positions p and q of the vertex cover.
    for (int m = 0; m < n; m++) {   // ∀m ∈ [1, n]
        for (int q = 0; q < k; q++) { // ∀p ∈ [1, k]
            for (int p = 0; p < q; p++) { // ∀q ∈ [1, k] with p < q
                Minisat::Lit x_mp = propositions[m][p];
                Minisat::Lit x_mq = propositions[m][q];
                // (¬x_{m,p} || ¬x_{m,q})
                solver->addClause(~x_mp, ~x_mq);  
            }   
        }        
    }

    //clauses3: No more than one vertex appears in the mth position of the vertex cover.
    // ∀m ∈ [1,k], ∀p,q ∈ [1,n] with p < q, a clause (¬x_{p,m} ∨ ¬x_{q,m})
    for (int m = 0; m < k; m++) { // ∀m ∈ [1,k]  
        for (int q = 0; q < n; q++) { //∀q ∈ [1,n]
            for (int p = 0; p < q; p++) { //∀p ∈ [1,n] with p < q
                Minisat::Lit x_pm = propositions[p][m];
                Minisat::Lit x_qm = propositions[q][m];
                // (¬x_{p,m} || ¬x_{q,m})
                solver->addClause(~x_pm, ~x_qm);  
            }   
        }        
    }

    //clauses4: Every edge is incident to at least one vertex in the vertex cover.
    // ∀⟨i,j⟩∈ E, a clause (x_{i,1} ∨ x_{i,2} ∨···∨ x_{i,k} ∨ x_{j,1} ∨ x_{j,2} ∨···∨ x_{j,k} )
    for (Edge e: edgeList) //∀⟨i,j⟩∈ E
    {
        Minisat::vec<Minisat::Lit> clauses;
        for (int l = 0; l < k; l++) { 
            //(x_{i,1} || x_{i,2} || ··· || x_{i,k})
            Minisat::Lit x_il = propositions[e.u][l];
            clauses.push(x_il);
            //(x_{j,1} || x_{j,2} || ··· || x_{j,k})
            Minisat::Lit x_jl = propositions[e.v][l];
            clauses.push(x_jl);
        }
        // (x_{i,1} || x_{i,2} || ··· || x_{i,k} || x_{j,1} || x_{j,2} ||···|| x_{j,k} )
        solver->addClause(clauses);
    }
    //================================================================================

    //std::cout << "=> nClauses = " << solver->nClauses() << std::endl;
    
    // check whether the CNF in the solver is still satisfiable
    bool satisfy = solver->solve();
    //std::cout << "=> satisfy = " << satisfy << std::endl;

    if (satisfy)
    {
        for (int v = 0; v < n; v++) 
        {
            for (int l = 0; l < k; l++) 
            {
                //the result of the solve method and the satisfying assignment that was found by the solver
                int satAssign = toInt(solver->modelValue(propositions[v][l]));
                if (satAssign == 0) // True is 0 for lbool. Bruh see in SolverTypes.h L124 #define l_True  (lbool((uint8_t)0))
                {
                    //Add back the vertex
                    cover.push_back(v);
					//std::cout << v << " ";
				}
                
            }
        }
        //std::cout << std::endl;
    }
    else
    {
        // Add -1 into the vector to indicate not satisfy
        // Why optional / varient do not work?
        //return NULL;
        cover.push_back(-1);
    }

    // de-allocates existing solver and allocates a new one in its place.
    solver.reset (new Minisat::Solver());

    return cover;
    
}

void FindMinimumVertexCoverLinearSearch(UndirectedGraph& graph)
{
    //Uses linear search to find minimum vertex cover

    // Get number of vertex
    int n = graph.GetSize();
    bool notSatisfy;
    std::vector<int> minimumCover;
    std::vector<int> cover;
    int shortest = INT_MAX;

    // vertex are from 1 to n
    // i is now 0 instead of 1 because we care about having no cover
    for (int i = 0; i < n; i++)
    {
        cover = FindVertexCover(graph, i);
        notSatisfy = (std::find(cover.begin(), cover.end(), -1) != cover.end());
        if (notSatisfy) 
        {
            //std::cout << "not found" << std::endl;
			continue;
		}
		else 
        {
            //std::cout << "found" << std::endl;
            if (cover.size() < shortest)
            {
                shortest = cover.size();
                minimumCover = cover;
            }
		}
    }
    PrintCover(minimumCover);
}

void PrintCover(std::vector<int> cover)
{
    //The output should just be a sequence of vertices in increasing order separated by one space each. 
    //You can use qsort(3) or std::sort for sorting.
    std::sort(cover.begin(), cover.end());
    for (int i = 0; i < cover.size(); i++) 
    {
        std::cout << cover[i] << " ";
    }
    std::cout << std::endl;
}