Input format of aspino

[mahi045]

I am trying to circumscriptino. Unfortunately, I cannot use it. I got the following parse error: PARSE ERROR! Unexpected char: n.
My input CNF file (toy.cnf) is very simple:

$ cat toy.cnf 
p cnf 2 1
1 2 0

Can you tell the correct input CNF format of circumscriptino?

[alviano]

Hi! Not DIMACS, but DIMACS-like. The prolog is ccnf, then there can be one line with objective literals (starting with 'o'), one line with "care literals" (starting with 'C', disjoint from objective literals; these literals are essentially used to group models), several lines with visible statements (starting with 'v'), several lines with cardinality constraints (starting with '+'), and several clauses (as in DIMACS). Below is Example 1 from "Model enumeration in propositional circumscription via unsatisfiable core analysis. Theory Pract. Log. Program. 17(5-6): 708-725 (2017)": p ccnf - o 1 2 3 0 v 1 x0 v 2 x1 v 3 x2 v 4 a v 5 b 4 1 0 -4 5 2 0 -4 -5 3 0 If variable a is not "don't care", the instance is enriched with C 4 0 and similarly if both a and b are not "don't care", the instance is enriched with C 4 5 0 Below is an example with a cardinality constraint (theory T3 from the same paper): p ccnf - o 6 7 0 v 1 x0 v 2 x1 v 3 x2 v 4 a v 5 b v 6 y1 v 7 y2 4 1 0 -4 5 2 0 -4 -5 3 0 + 2 -1 -2 -3 6 7 0 -7 6 0 Hope this may help. Let me know if I can clarify something else. All the best, Mario

…

On Sun, Apr 23, 2023 at 6:20 PM mahi045 ***@***.***> wrote: I am trying to circumscriptino. Unfortunately, I cannot use it. I got the following parse error: PARSE ERROR! Unexpected char: n. My input CNF file (toy.cnf) is very simple: $ cat toy.cnf p cnf 2 1 1 2 0 Can you tell the correct input CNF format of circumscriptino? — Reply to this email directly, view it on GitHub <#2>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA67ZMHNWSJ4BQD7MS6MH43XCVJF7ANCNFSM6AAAAAAXIT62DE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[mahi045]

Thanks for your information.
One clarification: does -n=0 option enumerate all minimal models?

[alviano]

There are two options:

…

-n is the number of models --circ-wit is the number of witnesses Both have default 1. Using -n=0 alone will produce one witness for each minimal assignment to the objective literals. If you want all witnesses, you should go with -n=0 --circ-wit=0. m

On Mon, Apr 24, 2023 at 6:18 PM mahi045 ***@***.***> wrote: Thanks for your information. One clarification: does -n=0 option enumerate all minimal models? — Reply to this email directly, view it on GitHub <#2 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA67ZMBEAP5AQYHYYI3B2O3XC2RWNANCNFSM6AAAAAAXIT62DE> . You are receiving this because you commented.Message ID: ***@***.***>