ECCC-Report TR12-069https://eccc.weizmann.ac.il/report/2012/069Comments and Revisions published for TR12-069en-usSat, 26 May 2012 12:22:52 +0300
Paper TR12-069
| On the complexity of computing minimal unsatisfiable LTL formulas |
francois hantry,
Mohand-Saïd Hacid,
Lakhdar Saïs
https://eccc.weizmann.ac.il/report/2012/069We show that (1) the Minimal False QCNF search problem (MF-search) and
the Minimal Unsatisfiable LTL formula search problem (MU-search) are FPSPACE complete because of the very expressive power of QBF/LTL, (2) we extend the PSPACE-hardness of the MF decision problem to the MU decision problem. As a consequence, we deduce a positive answer to the open question of PSPACE hardness of the inherent Vacuity Checking problem.
We even show that the Inherent Non Vacuous formula search problem is also FPSPACE-complete.
Sat, 26 May 2012 12:22:52 +0300https://eccc.weizmann.ac.il/report/2012/069