Unexpected results of simplify in ver. 2.2.0

[marekpiotrow]

I am using libcadical.a in UWrMaxSat. Yesterday I upgraded the library to the version 2.2.0. After running a sequence of tests I have observed unexpected results of the function simplify() on some instances, compared to the version 2.1.3. Namely, the number of irredundant clauses is not changing as much as in the previous version.

What could be the reason of that? Should I change the default value of some options?
Below, I attached some lines from logs for an instance.

ver. 2.1.3

[preprocessing-1] starting round 0 with 5886 variables and 1259604 clauses
[preprocessing-1] finished round 0 with 5886 variables and 419868 clauses
[preprocessing-2] starting round 1 with 5886 variables and 419868 clauses
[preprocessing-2] finished round 1 with 5886 variables and 419868 clauses
[preprocessing-3] starting round 2 with 5886 variables and 419868 clauses
[preprocessing-3] finished round 2 with 5886 variables and 419868 clauses

ver. 2.2.0

[preprocessing-0] starting with 5886 variables and 1259604 clauses
[preprocessing-0] finished with 5886 variables and 1259604 clauses
[preprocessing-1] starting round 0 with 5886 variables and 1259604 clauses
[preprocessing-1] finished round 0 with 5886 variables and 1259604 clauses
[preprocessing-2] starting round 1 with 5886 variables and 1259604 clauses
[preprocessing-2] finished round 1 with 5886 variables and 1259469 clauses
[preprocessing-3] starting round 2 with 5886 variables and 1259469 clauses
[preprocessing-3] finished round 2 with 5886 variables and 1259445 clauses

ver 2.2.0 with setting CADICAL_PREPROCESSLIGHT=false

[preprocessing-1] starting round 0 with 5886 variables and 1259604 clauses
[preprocessing-1] finished round 0 with 5886 variables and 1259604 clauses
[preprocessing-2] starting round 1 with 5886 variables and 1259604 clauses
[preprocessing-2] finished round 1 with 5886 variables and 1259482 clauses
[preprocessing-3] starting round 2 with 5886 variables and 1259482 clauses
[preprocessing-3] finished round 2 with 5886 variables and 1259457 clauses

[m-fleury]

I had a look at the code and this is not expected (we barely changed this part of the code) and from yours numbers it looks like we are eliminating fewer literals (or none actually) for some reason.

Could produce a trace (see below) and attach it here (or send it to me by email if it is too large)?

To produce a trace:

CADICAL_API_TRACE=/tmp/trace ./run-your-binary-here

[marekpiotrow]

I have just sent trace.tgz to your university mail.

[m-fleury]

Some comments about the trace itself:

• Resize:

resize 1
resize 2
...
resize 5884
resize 5885
resize 5886

You do not need to do this, you do not even need to call resize. CaDiCaL's add will take care of increasing the size. It is mostly useful if you know how big the instance and want to avoid doubling the size of various internal std::vector. But your version is not helping CaDiCaL.

• You have various calls to:

fixed 1270
assume 1270
limit decisions 1
solve

Depending on how often you do that, I think that using propagate () would be cheaper -- solve can be expensive even with a decision limit of 1.

At least, you are triggering a lot of calls to lucky (which you did not trigger before, because lucky did not support assumptions), which is able to find that your problem is SAT. But this is probably more expensive that you intended to. To restore the old behavior, you can set luckyassumptions to false.

Edit: and there is really something weird with elimination.

[m-fleury]

It is not elim, it is vivify:

c [vivify-1] flushed 836836 subsumed scheduled clauses

You are having duplicated clauses (3/4 apparently). So far vivify flushed them, but due to limits to the efforts, it does not anymore.

Actually, I have never seen vivifyflush being this useful ever before, but it is the fastest way to eliminate duplicated clauses. I have to think whether there is a better solution than just increasing the effort:

set vivifythresh 0
set vivifyeffort 10000
set vivifyschedmax 1000000

[marekpiotrow]

Thank you for the settings. It looks like they solve the problem with the instance. I will run more tests next week. The instance analyzed above is judgment-aggregation-ja-kemeny-preflib-00043-00000180.wcnf from Maxsat Evaluation 2023. It contains 1259604 lines with hard clauses (each of size 3) and the command sort -u does not eliminate any of them.

[m-fleury]

The literals are swapped, but there are duplicates:

$ less  judgment-aggregation-ja-kemeny-preflib-00043-00000180.wcnf | grep "^h" | sort | grep " 999" | grep -- "-996"
h -5109 999 -996 0
h -996 -5109 999 0
h 999 -996 -5109 0

I think that the best solution is that we add a new preprocessing technique that runs only once (per solve call) and remove duplicates. I will discuss this with Armin.

[arminbiere]

Right, we should have such an algorithm already as part of congruence closure. So we just need to make it a stand-alone procedure I assume called (in simplify) before congruence closure as in congruence closure it is restricted to those clauses duplicated due to substitution.

[marekpiotrow]

I wrote a small script and checked that all (15) weighted instances in the judgment-aggregation family of Maxsat Evaluation 2023 had 2/3 duplicated hard clauses. Moreover, also 6 unweighted ones (out of 25) of the family. The setting given above allowed UWrMaxSat to solve all of them in reasonable time.

But, I observed problems with another weighted family, namely tcp_wt-tcp_student_ ... . For example, tcp_wt-tcp_students_98_it_14.wcnf was solved by UWrMaxSat in 659s with library in 2.1.3 version, in 2124s in 2.2.0 version without the settings given above, but got timeout (3600s) in 2.2.0 with the settings. The trace of running:

CADICAL_API_TRACE=/tmp/trace-2.2.0set ./uwrmaxsat-2.2.0set -nm -no-scip -no-bin tcp_wt-tcp_students_98_it_14.wcnf -cpu-lim=3600

is attached.

trace-2.2.0set.gz

[m-fleury]

I have backported the deduplication algorithm (--deduplicateallinit) in the branch rel-2.2.0-backports. However, that is not helping for tcp_wt-tcp_student_. I am not sure why 2.1.3 was so much better. I am trying to find this out.

[marekpiotrow]

I have looked at the commit and, as far as I understand the code, it needs == 0 or negation in the second term in line 767 of internal.cpp to work. I changed it and run the test judgment-aggregation-ja-kemeny-preflib-00043-00000180.wcnf without the settings above and the duplicated clauses were removed.

[m-fleury]

Yes, I also realized that a bit later 43fbdf7

[m-fleury]

The simplification is part of 2.2.1, but I have not found out why cadical is slower.