C. P. Schnorr
- 1 Coot, S A The complexity of theorem-proving procedures Proc Third Annual ACM Syrup on Theory of Comptng , 1971, pp 151-158 Google Scholar
- 2 Coot, S A A hierarchy for non-deterministic time complexity Proc Fourth Annual ACM Symp on Theory of Computing, 1972, pp 187-192 Google Scholar
- 3 FISCHER, M J Lectures on network complextty Preprmt, U Frankfurt, 1974Google Scholar
- 4 HENmE, F C , AND STEARNS, R E Two-tape simulation of multttape Turmg machines J ACM 13, 4 (Oct 1966), 533-546 Google Scholar
- 5 KARP, R M Reduclbthty among combinatorial problems in Complextty of Computer Computattons, R E Miller and J W Thatcher, Eds , Plenum Press, New York, 1972, pp 85-104Google Scholar
- 6 KNUTH, D E The Art of Computer Programmtng, Vol 3. Sorting and Searchlng. Addtson-Wesley, Reading, Mass., 1973 Google Scholar
- 7 LEVIN, L.A Universal enumeration problems (m Russtan) Problemt Peredaci Informacu, Tom IX, 1972, pp 115-116Google Scholar
- 8 SC~NORR, C P The network complexity and the Turmg machine complexity of flmte functtons ACTA Informauca 7 (1976), 95-107Google Scholar
- 9 SCnNORR, C P A lower bound on the number of addmons an monotone computations. Theoretical Comptr. Sct 2 (1976), 305-315Google Scholar
- 10 SPECgER, R, AND STRASSEN, V Komplex~tat von Entsche~dungsproblemen Lecture Notes tn Computer Science, Vol 43, Sprmger-Verlag, Berhn, 1976 Google Scholar
Index Terms
- Satisfiability Is Quasilinear Complete in NQL
Recommendations
A satisfiability procedure for quantified boolean formulae
The renesse issue on satisfiabilityWe present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSATCNF of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a ...
Satisfiability of mixed Horn formulas
In this paper the class of mixed Horn formulas is introduced that contain a Horn part and a 2-CNF (conjunctive normal form) (also called quadratic) part. We show that SAT remains NP-complete for such instances and also that any CNF formula can be ...
Backjumping for quantified Boolean logic satisfiability
The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of ...
Comments