POLynomial hierARchy algorIthms and applicationS (POLARIS)

Type: National Project

Duration: from 2012 Jan 01 to 2015 Feb 28

Financed by: FCT

Prime Contractor: INESC-ID (Other)

The POLARIS project will develop a new generation of algorithms for decision problems complete for the polynomial-time hierarchy, and also for PSPACE-complete decision problems. All algorithms will be based on iterative calls to a SAT oracle, following the CEGAR-based paradigm. One of the main contributions will be to develop CEGAR-inspired algorithms for each restriction of QBF and also to the general QBF problem. Another main contribution will be to develop dedicated algorithms for representative problems in the lower levels of the polynomial-time hierarchy


  • INESC-ID (Other)

Principal Investigators