clingo_propagate_init_solver_literal returns "-1"

[mahi045]

I observed that clingo_propagate_init_solver_literal returns -1 for some aspif literals. As I observed, it is the only negative in my program.

Is literal -1 simply the negation of literal 1, or it bears some special meaning in the ASP program (e.g., -1 is true or false)?

Thanks in advance.

[rkaminsk]

Yes, literals are negated using -. The current implementation guarantees that the solver literals -1/1 are false/true.

[mahi045]

Thanks for your information. Another question: except “-1”, is it likely that clingo_propagate_init_solver_literal returns a negative literal (e.g., -2)?

[rkaminsk]

Thanks for your information. Another question: except “-1”, is it likely that clingo_propagate_init_solver_literal returns a negative literal (e.g., -2)?

Such kind of literals might be introduced during equivalence preprocessing. A simple example should be

{a}.
b :- not a.

Note that equivalence preprocessing is limited in some settings. In API mode, the solver is started by default in multi-shot mode, option --single-shot can be used to disable it. Equivalence preprocessing can also be disabled using option --eq=0. However it sometimes speeds up solving a lot and I not know if it completely prevents negative literals. I can also not say how likely negative literals are.