primer - prime implicants/implicates enumerator

Description

primer is a tool for prime implicants/implicates enumeration of non-clausal formulae.

The relevant publications are:

  1. Alessandro Previti, Alexey Ignatiev, Antonio Morgado and J. Marques-Silva: Prime Compilation of Non-clausal Formulae IJCAI 2015

News

Oct 12, 2015: New wiki page published for primer.

Distribution

Please contact Alessandro in case of any questions or problems.

Download binaries (Linux 64bit):

Example Usage

1. computation of all prime implicants and a cover of prime implicates:

 ./primer -pin-all INSTANCE-p.cnf INSTANCE-n.cnf 

2. computation of all prime implicates and a cover of prime implicants:

 ./primer -no-pin-all INSTANCE-p.cnf INSTANCE-n.cnf

Where INSTANCE-p.cnf and INSTANCE-n.cnf represent the CNF encoding of a non-clausal formula and its negation respectively. Note that each of the two files should contain in the first line:

  c n orig vars 'NUMBER-OF-ORIGINAL-VARS'
  

Where NUMBER-OF-ORIGINAL-VARS is the number of variables contained in the original formula before the encoding to CNF.

Contributors

Funding

The research on prime implicants/implicates enumeration and the development of primer were partially supported by Science Foundation Ireland

Print/export