README.md

Example Test Cases

This directory contains example input and output files demonstrating the unit propagation algorithm.

File Format

• .in files: Input clauses in CNF format (one clause per line, literals separated by spaces)
• .out files: Expected output showing discovered unit clauses in lexicographical order

Test Cases

1. Simple Propagation (simple_propagation)

Basic example showing cascading unit propagation.

Input:

a b
-a c
-c d
a

Explanation:

• Initial unit clause: a
• Propagating a removes clauses 1 and 4, and removes -a from clause 2, creating unit clause c
• Propagating c removes clause 2 and removes -c from clause 3, creating unit clause d

Output: a c d

---

2. Contradiction (contradiction)

Example that produces an empty clause (unsatisfiable).

Input:

a b
-b
b -a

Explanation:

• Initial unit clause: -b
• Propagating -b removes b from clauses, eventually producing an empty clause

Output: - (indicates contradiction)

---

3. Multiple Units (multiple_units)

Multiple initial unit clauses that don't interact.

Input:

x
y z
-y

Explanation:

• Initial unit clauses: x and -y
• Propagating -y removes it from clause 2, creating unit clause z

Output: x y z

---

4. Cascading Units (cascading_units)

Demonstrates a chain reaction of unit propagations.

Input:

a b c
-a d e
-d f
b

Explanation:

• b is a unit clause
• Propagating b removes clause 1
• Propagating -a from clause 2 produces d and e as units
• Propagating d removes clause 2 and produces f from clause 3

Output: b d e f

---

5. Lexicographic Order (lexicographic_order)

Verifies that output is sorted lexicographically.

Input:

p q
-p r
q
-r s

Explanation:

• Unit clauses discovered: q, r, s
• Must be output in alphabetical order

Output: q r s

---

6. Negated Literals (negated_literals)

Example with both positive and negated literals.

Input:

a -b
c
-a d

Explanation:

• Initial unit clause: c
• Propagating -a produces d as a unit clause

Output: c d

---

Running the Examples

Using Polynomial Implementation

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

Using Linear Implementation

cd LogicDirLinear
make
./dpll-linear < ../examples/simple_propagation.in

Testing All Examples

# From project root
for test in examples/*.in; do
    echo "Testing: $test"
    cd LogicDirPolynomial
    ./dpll-polynomial < ../$test
    cd ..
done

Understanding the Output

• Normal output: Space-separated list of unit clauses in lexicographical order
• Contradiction: Single dash - indicates an empty clause was produced
• No output: No unit clauses were found (shouldn't happen with these examples)

Creating Your Own Tests

1. Create a .in file with your CNF clauses (one per line)
2. Run it through either implementation
3. Verify the output matches your expectations
4. Create a corresponding .out file with the expected result

Remember:

• Each clause is a disjunction (OR) of literals
• The entire formula is a conjunction (AND) of clauses
• Literals starting with - are negated
• Unit clauses have only one literal