AIGER bridge

What it is

Authors

Armin Biere

Source of the author list

repository arminbiere/aiger

Language

C

Licence

MIT

Competitions

SAT Competition 2011 and later, as unrolled model checking and bit-vector instances

Repository

https://github.com/arminbiere/aiger.git

Pinned commit

5f8ce5ca5fc42a06e5d713309f99195a740ac2b4

Pinned git tree

7a9f000b9718b50d15bd9b7ab3cf7b889c50ddad

Seed

none: a bridge encodes a given circuit, it invents nothing

Notes

a bridge rather than a generator: it encodes the circuits another competition distributes. The models are fetched into a local cache by tools/fetch_upstream.py and never kept here. The number of time frames is the parameter that makes the family scale. The encoder is poormanaigtocnf, the plain Tseitin encoder of the aiger examples, which is what the 2011 submissions used: aigtocnf simplifies more and gives a different formula, which is why it is only available behind --optimised.

Build it and run it

docker build -t satex-gen/aiger:2021 bridges/aiger
docker run --rm satex-gen/aiger:2021 ...  > instance.cnf

The image can be published: the licence allows it.

Reference instances

30 with the same GBD hash · 1 with the same number of variables and clauses. Each line regenerates one known instance, from a competition or from the set its author published; the level says how close the result is. See verification.

Notes

• the model and the number of time frames are read from the file name; the circuit comes from the Hardware Model Checking Competition 2010