Back to Repositories

Testing Two-SAT Solver Implementation with Graph Theory in Algorithms Repository

This test suite validates the TwoSatSolverAdjacencyList implementation, focusing on boolean satisfiability problems using graph-based algorithms. The tests verify both satisfiable and unsatisfiable 2-SAT formulas through adjacency list representations.

Test Coverage Overview

The test suite provides comprehensive coverage of 2-SAT solver functionality through graph-based implementations.

Key areas tested include:

Simple satisfiable clauses
Impossible/unsatisfiable cases
Complex node cycles and graph relationships
Edge cases with single and multiple variable clauses

Implementation Analysis

The testing approach uses JUnit Jupiter to validate the TwoSatSolverAdjacencyList class functionality. Tests are structured around graph creation and clause addition patterns, utilizing Google Truth assertions for verification.

Implementation details include:

Graph initialization with dynamic node sizing
OR clause testing with variable negation
Complex clause relationship validation

Technical Details

Testing infrastructure includes:

JUnit Jupiter test framework
Google Truth assertion library
ArrayList-based graph representation
Helper methods for graph creation and manipulation

Best Practices Demonstrated

The test suite exemplifies strong testing practices through clear test case organization and comprehensive coverage.

Notable practices include:

Isolated test cases for specific scenarios
Clear test method naming conventions
Helper method abstraction for setup
Thorough edge case coverage

williamfiset/algorithms

src/test/java/com/williamfiset/algorithms/graphtheory/TwoSatSolverAdjacencyListTest.java

            
package com.williamfiset.algorithms.graphtheory;

import static com.google.common.truth.Truth.assertThat;

import java.util.*;
import org.junit.jupiter.api.*;

public class TwoSatSolverAdjacencyListTest {

  // Initialize graph with 'n' nodes.
  public static List<List<Integer>> createGraph(int n) {
    List<List<Integer>> graph = new ArrayList<>(2 * n);
    for (int i = 0; i < 2 * n; i++) graph.add(new ArrayList<>());
    return graph;
  }

  @Test
  public void testSimpleSatisfiable() {
    int n = 1;
    List<List<Integer>> g = createGraph(n);

    // Full clause: (p or ~p)
    TwoSatSolverAdjacencyList.addOrClause(g, 0, 0 ^ 1);

    TwoSatSolverAdjacencyList solver = new TwoSatSolverAdjacencyList(g);
    assertThat(solver.isSatisfiable()).isTrue();
  }

  @Test
  public void testSimpleImpossible() {
    int n = 1;
    List<List<Integer>> g = createGraph(n);

    // Full clause: (p or p) and (~p or ~p)
    TwoSatSolverAdjacencyList.addOrClause(g, 0, 0); // (p or p)
    TwoSatSolverAdjacencyList.addOrClause(g, 0 ^ 1, 0 ^ 1); // (~p or ~p)

    TwoSatSolverAdjacencyList solver = new TwoSatSolverAdjacencyList(g);
    assertThat(solver.isSatisfiable()).isFalse();
  }

  @Test
  public void testImpossibleFourNodeCycle() {
    int n = 2;
    List<List<Integer>> g = createGraph(n);

    // Full clause: (p0 or p1) and (p0 or ~p1) and (~p0 or p1) and (~p0 or ~p1)
    TwoSatSolverAdjacencyList.addOrClause(g, 2 * 0, 2 * 1); // (p0 or p1)
    TwoSatSolverAdjacencyList.addOrClause(g, 2 * 0, 2 * 1 ^ 1); // (p0 or ~p1)
    TwoSatSolverAdjacencyList.addOrClause(g, 2 * 0 ^ 1, 2 * 1); // (~p0 or p1)
    TwoSatSolverAdjacencyList.addOrClause(g, 2 * 0 ^ 1, 2 * 1 ^ 1); // (~p0 or ~p1)
    // System.out.println(g);

    TwoSatSolverAdjacencyList solver = new TwoSatSolverAdjacencyList(g);
    assertThat(solver.isSatisfiable()).isFalse();
  }
}