PA1 - Campaign Plan

Algorithms I

The Problem

To define his campaign plan, congressman Alan Turing decided to use public opinion gathered from Instagram polls. Each follower can vote for up to 2 proposals to keep in the plan, and up to 2 proposals to remove.

To satisfy all participants, it was decided that at least one proposal voted in favor by each person must be accepted, and at least one proposal voted against must be removed.

The problem is to determine whether there exists an assignment that satisfies these criteria and pleases all participants. You do not need to find a specific assignment, only to determine if one exists.

Modeling

This problem can be described as a 2-SAT satisfiability problem. We can construct a Boolean expression in conjunctive normal form (CNF), where each pair of votes forms a clause. Votes in favor are positive literals, and votes against are negated literals. If a vote contains a null literal, it is equivalent to a single literal clause; if both literals are null, the vote is ignored. Determining if this expression is satisfiable answers the original problem.

Each clause $(a \vee b)$ can be transformed into two implications:

• $(\neg a \rightarrow b)$
• $(\neg b \rightarrow a)$

Formula Example:

A clause $(x \vee \neg y)$ becomes:

• $(\neg x \rightarrow \neg y)$
• $(y \rightarrow x)$

ASCII Implication Graph:

  +---------+         +---------+
  |   x     |<--------|   y     |
  +---------+         +---------+
                    
                    
  +---------+-------->+---------+
  | not x   |         | not y   |
  +---------+         +---------+

Edges:

• y → x
• not x → not y

We represent these implications as edges in a directed graph.

For each variable $x$, we create two vertices: $x$ and $\neg x$. The implications become edges between these vertices.

The Boolean expression is unsatisfiable if and only if there is a path from any variable to its negation and back, i.e., both $x \rightarrow \neg x$ and $\neg x \rightarrow x$ exist. This means $x$ and $\neg x$ are in the same strongly connected component (SCC), which means the implications that generated them can't both be true at the same time.

Kosaraju's Algorithm

To check this efficiently, we use Kosaraju's algorithm to find SCCs in $O(V + E)$ time.

Steps:

1. Perform a DFS on the graph, recording the finish times of each vertex.
2. Reverse the graph.
3. Perform DFS in the order of decreasing finish times to identify SCCs.

If any variable and its negation are in the same SCC, the formula is unsatisfiable.

Data Structures and Implementation

• Graph: Represented as a vector of integer arrays, where each element is a vertex and the array contains outgoing edges.
• Stack: Used in Kosaraju's algorithm to store vertices by finish time (LIFO order).
• Arrays: Used to store the SCC of each vertex and to track visited vertices.

The main function is isPossible, which receives:

• Number of literals
• Number of clauses
• Two vectors representing the CNF expression (left and right sides of each clause)

It generates the implication graph and its reverse, runs Kosaraju's algorithm, and checks if any variable and its negation are in the same SCC. It outputs "no" if so, "yes" otherwise.

Input

The program reads a text file with:

• A line containing two integers: number of voters and number of proposals
• One line per voter, representing their votes as integers
• The end of input is marked by the line "0 0"

Execution

Use the command make all to build the executable tp01, then run it with the input file name as an argument:

./tp01 in.txt