DPLL Unit Propagation Algorithm - C Implementation

This project implements the Unit Propagation component of the Davis–Putnam–Logemann–Loveland (DPLL) algorithm in C. The DPLL algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in Conjunctive Normal Form (CNF).

Overview

The implementation focuses specifically on the unit propagation optimization technique, which is one of the key enhancements that makes DPLL more efficient than basic backtracking algorithms.

What is Unit Propagation?

Unit propagation is a constraint propagation technique where:

• If a clause contains only a single unassigned literal (a "unit clause"), that literal must be assigned true to satisfy the clause
• All clauses containing this literal become satisfied and can be removed
• The negation of this literal is removed from all remaining clauses
• This process cascades, often producing new unit clauses to propagate

Two Implementation Approaches

This project contains two different implementations of the unit propagation algorithm, each with different time complexity characteristics:

1. Polynomial Time Implementation (dpll-polynomial/)

Time Complexity: O(n²) where n is the number of clauses

A straightforward implementation that searches through all clauses to find unit clauses, then iterates through all clauses again to perform propagation. Simple and easy to understand, but slower for large inputs.

See detailed documentation →

2. Linear Time Implementation (dpll-linear/)

Time Complexity: O(n) where n is the number of literals

An optimized implementation using watched literals and a hash table for efficient clause tracking. Only examines clauses when necessary, achieving near-linear time complexity in practice. This is the approach used in modern SAT solvers.

See detailed documentation →

Comparison

Feature	Polynomial	Linear
Time Complexity	O(n²)	O(n)
Approach	Iterative search	Watched literals + hash table
Memory Usage	Lower	Higher (hash table overhead)
Code Complexity	Simpler	More complex
Best For	Small inputs, learning	Large inputs, performance

Input/Output Format

Input

Clauses in CNF format, one per line, with literals separated by spaces:

a b c
-a d
e
-b -c

• Positive literal: a
• Negated literal: -a
• Each line represents a disjunction (OR) of literals
• The entire input represents a conjunction (AND) of clauses

Output

The program outputs discovered unit clauses in lexicographical order:

a d e

Special case - if a contradiction (empty clause) is detected:

-

Example

Input:

a b
-a c
-c d
a

Execution:

1. Initial unit clause: a
2. Remove clauses containing a: eliminates clauses 1 and 4
3. Remove -a from clause 2: produces new unit clause c
4. Remove clauses containing c: eliminates clause 2
5. Remove -c from clause 3: produces new unit clause d

Output:

a c d

Building and Running

Polynomial Implementation

cd dpll-polynomial
make                            # Compile the code
./dpll-polynomial < input.in    # Run with input file
make clean                      # Clean build artifacts

Linear Implementation

cd dpll-linear
make                            # Compile the code
./dpll-linear < input.in        # Run with input file
make clean                      # Clean build artifacts

Examples

Sample test cases are provided in the examples/ directory. Each example includes:

• .in file: Input clauses in CNF format
• .out file: Expected output
• README.md: Detailed explanations of each test case

Try running an example:

cd dpll-polynomial
./dpll-polynomial < ../examples/simple_propagation.in

See examples/README.md for more details.

Project Structure

DPLL_unit_propagation/
├── dpll-polynomial/             # O(n²) implementation (Task 1)
│   ├── main.c                   # Entry point
│   ├── UnitPropagationAlgorithm.c  # Core algorithm
│   ├── Clauses.c/h              # Clause management
│   ├── Literals.c/h             # Unit clause storage
│   ├── List.c/h                 # Singly-linked list
│   ├── ListNode.c/h             # List node implementation
│   ├── StorageStructure.c/h     # Dynamic array
│   ├── Makefile
│
├── dpll-linear/                 # O(n) implementation (Task 3)
│   ├── mainLinear.c             # Entry point
│   ├── UnitPropagationAlgorithm.c  # Core algorithm with watch literals
│   ├── Clauses.c/h              # Clause management
│   ├── Literals.c/h             # Unit clause storage
│   ├── HashTable.c/h            # Literal → Clause mapping
│   ├── List.c/h                 # Doubly-linked list with watch pointers
│   ├── ListNode.c/h             # List node with value tracking
│   ├── StorageStructure.c/h     # Dynamic array
│   ├── Makefile
│
└── README.md                    # This file

Key Differences Between Implementations

Feature	Polynomial	Linear
Time Complexity	O(n²)	O(n)
List Structure	Singly-linked	Doubly-linked
Clause Tracking	Full scan each iteration	Hash table lookup
Watch Literals	No	Yes (two per clause)

Project Structure

DPLL_unit_propagation/
├── dpll-polynomial/             # O(n²) implementation
│   ├── README.md                # Detailed documentation
│   ├── *.c, *.h                 # Source files
│   └── Makefile
│
├── dpll-linear/                 # O(n) implementation
│   ├── README.md                # Detailed documentation
│   ├── *.c, *.h                 # Source files
│   └── Makefile
│
├── examples/                    # Test cases with explanations
│   ├── README.md
│   └── *.in, *.out
│
├── LICENSE                      # MIT License
└── README.md                    # This file