Solvable SAT

Solvable SAT

Posted October 15, 2014 by in Uncategorized

Check out Meet in the middle tutorial!

Meet in the middle

View Post on Quora

Posted April 1, 2014 by in Uncategorized

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

Problem: Divisibility

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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

Strategy: Hard problem

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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

Strategy: Don't trust the writer

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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

Strategy: Solve backwards, Think in reverse!

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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

Strategy: Special points in the search space

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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

Strategy: Simplify the problem

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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

Strategy: Focus on the solution

View Post on Quora

Posted March 14, 2014 by in Uncategorized

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.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 {
StringTokenizer strtok;
int tc = Integer.parseInt(strtok.nextToken());
while (tc-- > 0) {
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++) {
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");
}
}
}
```

Posted November 3, 2013 by in Uncategorized