Skip to content

README.md

Latest commit

 

History

History
20 lines (14 loc) · 698 Bytes

README.md

File metadata and controls

20 lines (14 loc) · 698 Bytes

Installation

  1. get picosat, follow its installation instructions
  2. modify the Makefile (adjust LIBS and INCLUDE to your needs)
  3. issue make

Usage

Works on DIMACS files whose first comment line contains the number of free variables f. Enum expects that variables 1..f are free, all the over variables are considered bound. Example:

c 3
p cnf 5 1
1 2 3 4 5 0

is used for ∃ x4, x5. x1 ∨ x2 ∨ x3 ∨ x4 ∨ x5. The QE approach is inspired by Brauer, King, Kriener: Existential Quantification as Incremental SAT, CAV 2011.