algorithm - 2-SATisfiabilty问题测试用例

Question

我已经为 2-satisfiability 问题编写了一个 SAT 求解器，有人请给我一个测试用例，比如 10000 个文字，它只有一个可满足的分配，即只有一个解决方案

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

这种方法有效吗？

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

这只有在 a 为真时才能满足。

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

只有当 b 为假时才能满足。因此

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

完全指定 a 和 b 的值。我们现在可以将它扩展到任意数量的文字。

要测试您的应用程序，您还可能指定相互矛盾的要求，因此没有解决方案。