Post by Mahmoud Radwan:

Solvable SAT

Solvable SAT

Check out Meet in the middle tutorial!

Post by Mahmoud Radwan:

Meet in the middle

View Post on Quora

Checkout analysis for problem Divisibility (6200 on ACM ICPC Live archive, UVa online judge 12581 )

Post by Mahmoud Radwan:

Problem: Divisibility

View Post on Quora

Check out "Hard problem" problem solving strategy on my Quora blog!

Post by Mahmoud Radwan:

Strategy: Hard problem

View Post on Quora

Check out "Dont trust the writer" problem solving tip on my Quora blog!

Post by Mahmoud Radwan:

Strategy: Don't trust the writer

View Post on Quora

Check out "Think backwards, Think in reverse" problem solving strategy on my Quora blog!

Post by Mahmoud Radwan:

Strategy: Solve backwards, Think in reverse!

View Post on Quora

Checkout "Special points in the search space" on my quora blog

Post by Mahmoud Radwan:

Strategy: Special points in the search space

View Post on Quora

Check out "simplify the problem" problem solving strategy on my quora blog

Post by Mahmoud Radwan:

Strategy: Simplify the problem

View Post on Quora

Check out Focus on the solution problem solving strategy on my quora blog

Post by Mahmoud Radwan:

Strategy: Focus on the solution

View Post on Quora

This is an interesting 2-Sat problem, get familiar with the problem here
Check out last seven slides here for more understanding how to solve the problem.
Now how do we approach a problem using 2-Sat, its usually easier to think of it as implications, think what happens when you Don’t satisfy something, what should be done to still make things work.
Lets apply this to the problem we have here
So we have a simple route request from (i0,j0) to (i1,j1) where i1 > i0, j0 > j1
what would happen if we had the street i0 going west only ? then the route would need to go (i0,j0) -> (i1,j0) -> (i1,j1) which requires that j0 is south and i1 is east.
so now we know that
i0 west implies j0 south and i0 west implies i1 east
which is the same as saying
(i0 east or j0 south) AND (i0 east or i1 east)
we should repeat this for i1, j0 and j1.
if we supply all the constraints we’ll have a 2-Sat, here’s the code.

import java.io.BufferedReader;
import java.io.InputStreamReader;
import java.util.Arrays;
import java.util.StringTokenizer;

public class Manhattan_10319 {
	static class SlowTwoSatSolver {
		byte[][] graph;

		public SlowTwoSatSolver(int nvars) {
			graph = new byte[nvars * 2][nvars * 2];
		}

		public void addImplication(int x, int v_x, int y, int v_y) {
			graph[x * 2 + v_x][y * 2 + v_y] = 1;
		}

		public boolean solve() {
			int n = graph.length;
			for (int k = 0; k < n; k++)
				for (int i = 0; i < n; i++)
					for (int j = 0; j < n; j++)
						graph[i][j] |= graph[i][k] & graph[k][j];
			for (int i = 0; i < n; i++)
				if ((graph[i][i ^ 1] & graph[i ^ 1][i]) == 1)
					return false;
			return true;
		}
	}

	public static void main(String[] args) throws Exception {
		BufferedReader in = new BufferedReader(new InputStreamReader(System.in));
		StringTokenizer strtok;
		strtok = new StringTokenizer(in.readLine());
		int tc = Integer.parseInt(strtok.nextToken());
		while (tc-- > 0) {
			strtok = new StringTokenizer(in.readLine());
			int n = Integer.parseInt(strtok.nextToken());
			int m = Integer.parseInt(strtok.nextToken());
			int r = Integer.parseInt(strtok.nextToken());
			SlowTwoSatSolver solver = new SlowTwoSatSolver(n + m);
			for (int i = 0; i < r; i++) {
				strtok = new StringTokenizer(in.readLine());
				int i0 = Integer.parseInt(strtok.nextToken()) - 1;
				int j0 = Integer.parseInt(strtok.nextToken()) - 1;
				int i1 = Integer.parseInt(strtok.nextToken()) - 1;
				int j1 = Integer.parseInt(strtok.nextToken()) - 1;
				int di = i1 - i0;
				int dj = j1 - j0;
				if (di == 0 && dj == 0) {
					continue;
				} else if (di == 0) {
					int dir = dj > 0 ? 1 : 0;
					solver.addImplication(i0, dir ^ 1, i0, dir);
				} else if (dj == 0) {
					int dir = di > 0 ? 1 : 0;
					solver.addImplication(n + j0, dir ^ 1, n + j0, dir);
				} else {
					int dir0 = dj > 0 ? 1 : 0;
					int dir1 = di > 0 ? 1 : 0;
					solver.addImplication(i0, dir0 ^ 1, i1, dir0);
					solver.addImplication(i0, dir0 ^ 1, n + j0, dir1);

					solver.addImplication(i1, dir0 ^ 1, i0, dir0);
					solver.addImplication(i1, dir0 ^ 1, n + j1, dir1);

					solver.addImplication(n + j0, dir1 ^ 1, n + j1, dir1);
					solver.addImplication(n + j0, dir1 ^ 1, i0, dir0);

					solver.addImplication(n + j1, dir1 ^ 1, n + j0, dir1);
					solver.addImplication(n + j1, dir1 ^ 1, i1, dir0);
				}
			}
			if (solver.solve())
				System.out.println("Yes");
			else
				System.out.println("No");
		}
	}
}