Bug Observation
Correct answer for the following test case.
p cnf 5 6
e 1 0
e 3 0
r 0.285714 2 0
r 0.461538 4 0
r 0.307692 5 0
-2 -1 0
2 1 0
1 -4 -3 0
1 4 3 0
-1 -5 -3 0
-1 5 3 0
But if I add a unit clause.
The answer will be 0 (wrong answer).
However, the following test case will be correct.
p cnf 2 3
e 1 0
r 0.285714 2 0
-2 -1 0
2 1 0
-1 0
Code Modification
I try to fix it by remove line 166 in src/ssat/core/SsatSolver.cc.
And add else condition to line 168~172 as
// save unit clauses
if (lits.size() == 1) {
unitClause.push();
lits.copyTo(_unitClause.last());
}
else
S.addClause_(lits);This modification makes the above instance correct.
But the solver cannot solve sand-castle benchmarks.
Bug Observation
Correct answer for the following test case.
But if I add a unit clause.
The answer will be 0 (wrong answer).
However, the following test case will be correct.
Code Modification
I try to fix it by remove line 166 in src/ssat/core/SsatSolver.cc.
And add else condition to line 168~172 as
This modification makes the above instance correct.
But the solver cannot solve sand-castle benchmarks.