Circumscriptino

Circumscriptino is a solver for propositional circumscription.

Static binary for Linux 64-bits: [circumscriptino-static].
Source code: [GitHub (aspino project)].
Examples: [examples.zip].
Benchmarks: [abstraction-refinement-intel.tar.bz2], [atpg.tar.bz2], [bioinfo-satcomp09.tar.bz2], [bmc-aerielogic.tar.bz2], [bmc-default.tar.bz2], [design-debugging.tar.bz2], [equivalence-checking.tar.bz2], [fpga-routing.tar.bz2], [hardware-verification.tar.bz2], [intervention.tar.bz2], [product-configuration.tar.bz2], [software-verification.tar.bz2].

$ ./circumscriptino-static --help
usage: ./circumscriptino-static [flags] [input-file]

OPTIONS:
  -n            =   [   0 .. imax] (default: 1)
  --circ-wit    =   [   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 care literals, are used to group interpretations.

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, care literals are specified as a DIMACS clause preceded by 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