# circumscriptino

Circumscriptino is a solver for propositional circumscription.

Static binary for Linux 64-bits: [circumscriptino-static].

Source code: [GitHub (aspino project)].

Examples: [examples.zip].

```
$ ./circumscriptino-static --help
usage: ./circumscriptino-static [flags] [input-file]
OPTIONS:
-n = <int32> [ 0 .. imax] (default: 1)
--circ-wit = <int32> [ 0 .. imax] (default: 1)
--help Print help message.
```

Circumscription applies to a theory T and sets P,Z of atoms. Atoms in P are subject to minimization, and called objective literals (in fact, for circumscriptino P may also include negative literals). Atoms in Z are irrelevant, and atoms neither in P nor in Z, called

The input format of circumscriptino is similar to DIMACS. The preamble is the following:

`p ccnf -`

(Actually, also `p ccnf +`

can be used, to maximize objective literals.)

Objective literals are specified as a DIMACS clause preceded by `o`

:

`o <space-separated list of literals> 0`

Similarly, `C`

:

`C <space-separated list of literals> 0`

Literals can also be associated with names (or strings), so to pretty print models:

`v <literal> <string>`

Finally, the input may comprise DIMACS clauses and cardinality constraints. Cardinality constraints have the following form:

`+ <bound> <space-separated list of literals> 0`

The cardinality constraint is satisfied by an interpretation I if the intersection of the list of literals with the interpretation has cardinality greater or equal to the bound.

Models are printed as space-separated lists of strings associated with true literals. Each model is preceded by `v`

.

Here is the output of circumscriptino for some examples:

```
$ cat t1.ccnf
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
$ ./circumscriptino-static -n=0 --circ-wit=0 t1.ccnf
v x0
v x0 b
v x2 a b
v x1 a
$ cat t1ab.ccnf
p ccnf -
o 1 2 3 0
C 4 5 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
$ ./circumscriptino-static -n=0 --circ-wit=0 t1ab.ccnf
v x0
v x0 b
v x2 a b
v x1 a
$ cat t2.ccnf
p ccnf -
o 1 2 3 0
v 1 x0
v 2 x1
v 3 x2
v 4 a
v 5 b
v 6 r
4 1 0
-4 5 2 0
-4 -5 3 0
-6 1 0
-6 2 0
-6 3 0
$ ./circumscriptino-static -n=0 --circ-wit=0 t2.ccnf
v x0
v x0 b
v x2 a b
v x1 a
$ cat t2r.ccnf
p ccnf -
o 1 2 3 0
C 6 0
v 1 x0
v 2 x1
v 3 x2
v 4 a
v 5 b
v 6 r
4 1 0
-4 5 2 0
-4 -5 3 0
-6 1 0
-6 2 0
-6 3 0
$ ./circumscriptino-static -n=0 --circ-wit=0 t2r.ccnf
v x0
v x0 b
v x1 a
v x2 a b
v x0 x1 x2 a b r
v x0 x1 x2 a r
v x0 x1 x2 r
v x0 x1 x2 b r
$ cat t3.ccnf
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
$ ./circumscriptino-static -n=0 --circ-wit=0 t3.ccnf
v x1 a
v x0
v x0 b
v x2 a b
```