2-SATisfiabilty problem test cases

Question

I have written a SAT solver for 2-satisfiability problem,someone please provide me a test case with say 10000 literals which has only one satisfiable assignment i.e only one solution

The format can be:(for 3 literals)
2            // No of clauses and then each clause
2 3
1 -2
corresponding to
(b+c).(a+!b)

Answer 1

Test coverage is usually difficult, most of the times, you just forget about a factor or another.

I usually proceeds in few steps:

1. Make sure that it solves a trivial problem (or some)
2. Test Edge Cases / Boundary conditions: 0 clause for example
3. Test Error Cases: badly formatted input, problems with no solution
4. Test Performance / Mass Injection (see if the program does not crash under load, does not leak, ...)

2) and 3) are pretty much interchangeable, 4) should only come if you have ways to investigate this kind of information (benchmarking, memory leak detection...).

An important point is that you should not reverse engineer your code to write the tests, because you would end up testing your code, but not testing that it obeys the specifications.

If it's a home project, specifications are usually informal but they still exist (in your head) and this is after them that you should produce the test cases.

Answer 2

Does this approach work?

 (a + b ).(a + !b) 

This can only be satisified if a is true.

 (a + !b).(!a + !b)

Can only be satisfied if b is false. Hence

  (a + b ).(a + !b).(a + !b).(!a + !b)

Completely specifies values for a and b. We can now extend this for any number of literals.

To test your app you might also specify contradictory requriements, hence something with no solution.