README.md

Polynomial Time Unit Propagation Implementation

This is a straightforward O(n²) implementation of the unit propagation algorithm, focusing on clarity and simplicity.

Time Complexity

O(n²) where n is the number of clauses

Algorithm Overview

The algorithm uses a simple iterative approach:

1. Search Phase: Scan through all clauses to find a unit clause
2. Propagation Phase: When a unit clause is found:
   • Store the unit clause
   • Remove all clauses containing this literal
   • Remove the negated literal from remaining clauses
   • Check if an empty clause is produced (contradiction)
3. Repeat: Continue until no more unit clauses exist

Pseudocode

do:
  unitClauseFound = false
  for each clause in clauses:
    if clause has only 1 literal:
      unitClauseFound = true
      unitClause = that literal
      store unitClause
      remove clause from clauses
      propagate(unitClause)
      if empty clause produced:
        return CONTRADICTION
      break
while unitClauseFound

Data Structures

Core Components

• StorageStructure: Dynamic array that grows as needed using realloc()
  • Stores either strings (literals) or lists (clauses)
  • Initial capacity: defined by STARTING_ARRAY_SIZE
• List: Singly-linked list representing literals in a clause
  • Each node contains a literal string
  • Supports insertion at start and removal by index
• Clauses: Container managing all input clauses
  • Uses StorageStructure to store array of List*
  • Provides getUnitClauses() method to run the algorithm
• Literals: Container storing discovered unit clauses
  • Uses StorageStructure to store array of strings
  • Handles output formatting in lexicographical order

File Structure

main.c                        # Entry point, input parsing
UnitPropagationAlgorithm.c    # Core propagation logic
Clauses.c/h                   # Clause container and algorithm controller
Literals.c/h                  # Unit clause storage and output
List.c/h                      # Singly-linked list implementation
ListNode.c/h                  # List node structure
StorageStructure.c/h          # Dynamic array implementation

Detailed Algorithm Flow

1. Input Processing (main.c)

// Read clauses line by line
while getline() succeeds:
  parse line into tokens
  create new List for this clause
  for each token:
    insert literal at start of list
  add list to clauses array

2. Unit Propagation (UnitPropagationAlgorithm.c)

The unitPropagation() function handles a single unit clause:

unitPropagation(clauses, unitClause):
  negatedUnitClause = findNegated(unitClause)

  for each clause:
    for each literal in clause:
      if literal == unitClause:
        remove entire clause
        break
      else if literal == negatedUnitClause:
        if clause has only 1 literal:
          return EMPTY_CLAUSE  // Contradiction!
        else:
          remove literal from clause

3. Main Loop (Clauses.c)

The getUnitClauses() function coordinates the overall process:

getUnitClauses():
  do:
    unitClauseFound = false
    for i = 0 to numberOfClauses:
      if clause[i].numberOfLiterals == 1:
        unitClauseFound = true
        unitClause = copy(clause[i].head.literal)
        store unitClause in literals
        remove clause[i] from clauses
        result = unitPropagation(clauses, unitClause)
        if result == EMPTY_CLAUSE:
          return EMPTY_CLAUSE
        break
  while unitClauseFound
  return SUCCESS

Complexity Analysis

Time Complexity: O(n²)

• Outer loop: Runs O(n) times (worst case: each clause becomes unit)
• Unit clause search: O(n) - must scan all remaining clauses
• Propagation per unit: O(n·m) where m is average literals per clause
  • Visit each clause: O(n)
  • Check each literal: O(m)
• Total: O(n) × O(n) = O(n²)

Space Complexity: O(n·m)

• Store n clauses with m literals each
• Dynamic arrays grow by reallocation
• Singly-linked lists for each clause

Key Implementation Details

Memory Management

All dynamic memory is properly managed:

• strdup() creates copies of string literals
• Each structure has a freeMemory() function pointer
• Lists are freed recursively (node by node)
• Storage structures free their arrays and contents

String Negation

The findNegatedUnitClause() function handles two cases:

• If literal starts with -: remove it (e.g., -a → a)
• Otherwise: prepend - (e.g., a → -a)

Array Management

StorageStructure provides a generic dynamic array:

• Can store either strings or lists (via Type enum)
• Automatically grows using realloc() when capacity reached
• removeFromArray() shifts elements to maintain contiguous storage

Building and Running

Compile

make

Run

./dpll-polynomial < input_file.in

Clean

make clean

Example Walkthrough

Input:

a b
-a c
-c d
a

Execution:

1. Initial state:

   • Clause 0: {a, b}
   • Clause 1: {-a, c}
   • Clause 2: {-c, d}
   • Clause 3: {a} ← unit clause!

2. Process unit clause a:

   • Store a in literals
   • Remove clause 0 (contains a)
   • Remove clause 3 (contains a)
   • Remove -a from clause 1 → produces {c} (new unit!)
   • Remaining clauses: {c}, {-c, d}

3. Process unit clause c:

   • Store c in literals
   • Remove clause with {c}
   • Remove -c from remaining clause → produces {d} (new unit!)
   • Remaining clauses: {d}

4. Process unit clause d:

   • Store d in literals
   • Remove clause with {d}
   • Remaining clauses: none

5. Output: a c d

Advantages

• Simple to understand: Clear, straightforward logic
• Easy to debug: Direct correspondence between code and algorithm
• Low memory overhead: Only essential data structures
• Correct: Handles all edge cases properly

Disadvantages

• Slower for large inputs: O(n²) complexity becomes problematic
• Redundant scanning: Examines clauses that haven't changed
• Physical removal: Array shifting on every deletion

Comparison to Linear Implementation

This implementation prioritizes clarity over performance. For large-scale SAT solving, the linear implementation (using watched literals) is significantly faster, but this version is excellent for:

• Learning the unit propagation algorithm
• Small to medium input sizes
• Situations where code simplicity matters more than performance