Understanding output

[uler3161]

I'm new to using cadical. Using the command line tool, I'm having some problems understanding console output and simplified CNF output (-o argument)

There's a lot of stuff on the console output that I don't understand, but I'm mostly interested in the remaining variables. For instance, here's some output:

c  seconds   reductions  redundant   irredundant
c          MB    restarts       trail         variables
c           level   conflicts       glue            remaining
c
c *  3.87 698  0 0   0    0    0  0% 0 4186632 1668313 100%
c {  4.96 725  0 0   0    0    0  0% 0 4186632 1668313 100%
c -  6.31 726 412 1  20  300  290  2% 2 4186182 1668313 100%
c }  6.52 726 417 1  78 1001  938  1% 3 4186182 1668313 100%
c [  6.52 726  0 1  78 1001  938  0% 0 4186182 1668313 100%
c O  7.28 740 31 1  78 1002  939 100% 23 4186182 1668313 100%
c i 13.24 740 29 1  78 1012  948 100% 21 4186182 1668307 100%
c - 117.51 877 36 2  78 1873 1721 23% 15 4186162 1668307 100%
c s 177.93 856 56 2  79 2655 2444 21% 18 4186162 1668307 100%
c v 180.44 934 56 2  79 2655 2444 21% 18 4186162 1668307 100%
c w 180.80 934 56 2  79 2655 2442 21% 18 4186162 1668307 100%
c t 182.10 934 56 2  79 2655 2442 21% 18 4171132 1668307 100%
c e 191.04 883 56 2  79 2655  233 21% 18 1516323 317601 19%
c s 192.02 882 56 2  79 2655  231 21% 18 1428141 317601 19%
c e 193.68 882 56 2  79 2655  229 21% 18 1428130 316623 19%

1. When it says 19%, does that mean it's found assignments for the other 81% of variables?
2. If so, are those the final assignments for those variables? Or does it mean that if a conflict is found, it's going to backtrack and that 19% might go back up to a higher percentage?

The other thing I'm trying to understand is the -o argument. I was using it with the -t option in an attempt to go to a certain point, then write out the file, but it's flaky. Sometimes it writes to the file, sometimes it doesn't. Had better luck with putting in a decision limit with -d. Specifically I put in a limit that would get me to the 19% remaining variables in my above example.

So, what is confusing about -o is I'm not sure I understand what the output file is representing.

1. It's supposed to be a simplified dimacs file. Does that mean it's found clauses in the original dimacs that are useless and has filtered those out?
2. If the simplified dimacs is sat, that proves the original is sat?
3. A solution to the simplified dimacs will also solve the original?

Sorry for all the questions. Just trying to get up to speed quickly on how this all works. Thanks.

[m-fleury]

SAT solvers like CaDiCaL do two major kind of things:

• CDCL (where new clauses are learnt, conflicts are found)
• simplification called pre- and inprocessing where the formula is transformed and (hopefully) simplified such that CDCL works better. For more details, see the Handbook chapter. These transformation preserve satisfiability (sat before = sat after) but models after must be fixed to be models before (see for example, Fazekas et al. SAT'19).

19% means that 81% have been removed, which is here done by variable elimination (indicated by the e after the 'c' at the beginning of the line). Until the next release this number cannot go up. Starting with the next release (rc2 currently), it can go up due to variable addition (and can be larger than 100% actually).

Limitation based on conflicts with -c is easier because the number of conflicts is indicated in the output. And it is not random unlike -t which is based on time.

To your questions:

1. -o dumps the current state of the formula. Some clauses will be removed (or simplified) but also some literals.
2. Yes.
3. No (you need model reconstruction to fix this, but -o does not provide enough information how to do that).

Sorry for all the questions. Just trying to get up to speed quickly on how this all works. Thanks.

Look at a talk on SAT solving given at a summer school, like this one.

[uler3161]

Thanks for all the info. It clarifies things a bit. I'll spend some time looking at the links you provided.