algorithm - 2-SATisfiability問題のテストケース

Question

私は2充足可能性問題のSATソルバーを作成しました。誰かが、充足可能な割り当てが1つだけ、つまりソリューションが1つしかない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

テストカバレッジは通常困難であり、ほとんどの場合、何らかの要因を忘れるだけです。

私は通常、いくつかのステップで進みます。

1. それが些細な問題（またはいくつか）を解決することを確認してください
2. テストエッジケース/境界条件：たとえば0句
3. テストエラーケース：入力の形式が正しくない、解決策がない問題
4. テストパフォーマンス/マスインジェクション（プログラムが負荷の下でクラッシュしないか、リークしないかを確認してください...）

2）と3）はほとんど互換性があり、4）この種の情報を調査する方法（ベンチマーク、メモリリーク検出など）がある場合にのみ使用する必要があります。

重要な点は、コードをリバースエンジニアリングしてテストを記述しないようにすることです。これは、コードをテストすることになりますが、仕様に準拠していることをテストしないためです。

ホームプロジェクトの場合、仕様は通常非公式ですが、（頭の中に）まだ存在しているため、テストケースを作成する必要があります。

Answer 2

このアプローチは機能しますか？

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

これは、aが真の場合にのみ満たすことができます。

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

bがfalseの場合にのみ満たすことができます。したがって、

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

aとbの値を完全に指定します。これを任意の数のリテラルに拡張できるようになりました。

アプリをテストするために、矛盾する要件を指定することもできます。そのため、解決策がありません。