search

niklasso / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
1.02k stars 390 forks source link

analyzeFinal's returned clause is not minimal #11

Closed msoos closed 10 years ago

msoos commented 10 years ago

If the 2nd assumed literal has been set to the opposite value at zero level, the conflict returned should only contain that literal. However, it may contain the other (1st) literal assumed, too. As an extreme example, if there are 100 other literals assumed, and the one set at 0 decision level is the 101th, the returned conflict may contain 101 literals.

niklasso commented 10 years ago

Mate,

I'm not able to repeat this. Can you be more specific with how to trigger this?

Thanks for the report, Niklas

On Fri, Jan 17, 2014 at 10:49 PM, Mate Soos notifications@github.comwrote:

If the 2nd assumed literal has been set to the opposite value at zero level, the conflict returned should only contain that literal. However, it may contain the other (1st) literal assumed, too. As an extreme example, if there are 100 other literals assumed, and the one set at 0 decision level is the 101th, the returned conflict may contain 101 literals.

— Reply to this email directly or view it on GitHubhttps://github.com/niklasso/minisat/issues/11 .

msoos commented 10 years ago

I didn't actually produce this, I was just looking at this code and realized it. Here is the scenario:

We are now returning an out_conflict that contains two literals. It should only contain one, v2.

niklasso commented 10 years ago

Mate,

We will only get to the condition "reason(x) == CRef_Unef" for variables that are marked as seen. As you say, nothing is marked. In fact, it will never mark anything from level 0 and thus the only literal from level 0 that can be in the result is 'p' itself. Right?

/Niklas

On Mon, Jan 20, 2014 at 4:26 PM, Mate Soos notifications@github.com wrote:

I didn't actually produce this, I was just looking at this code and realized it. Here is the scenario:

  • assumps contains: "v1 -v2"
  • v1 is unset
  • v2 has been set to TRUE at decision level 0 through a conflict.
  • We are now after the conflict, decision level is 0.
  • v1 is picked as 1st decison literal due to while (decisionLevel() < assumptions.size()){...
  • v1 is propagated, nothing propagates.
  • as before, but }else if (value(p) == l_False){analyzeFinal(~p, conflict); now triggers on p = -v2.
  • v2 is added to out_conflict in analyzeFinal in line 469
  • seen[v2] is set.
  • Now line 466 goes through the trail in reverse order: for (int i = trail.size()-1; i >= trail_lim[0]; i--){.
  • Nothing in seen[] will be set, as nothing was propagated through v1
  • if (reason(x) == CRef_Undef){ will fire for v1
  • v1 is added to out_conflict (line 471)

We are now returning an out_conflict that contains two literals. It should only contain one, v2.

— Reply to this email directly or view it on GitHubhttps://github.com/niklasso/minisat/issues/11#issuecomment-32768310 .

msoos commented 10 years ago

Ahh, thanks for the explanation. I'm sorry to have bothered you. By the way, do you have a fuzzer/tester for this? I'm struggling to get some things right in my solver and testing is the hardest part. My tester harness is already +1000 LoC but it still doesn't test the returned conflict clause.

On a side-note, I was thinking about asking the community to come up with a newer DIMACS: winning the race doesn't guarantee that the system that won is usable in the real world. Library usage (i.e. calling solve() multiple times) assumptions and returned conflicts are not tested at all. What do you think?

msoos commented 10 years ago

The issue was a non-issue. Thanks for the explanation and the answers! Closing.