The Propositional Formula Checker HeerHugo

Aho, A. V., Hopcroft, J. E. and Ullman, J. D.: Data Structures and Algorithms, Addison-Wesley, 1987.

Aspvall, B., Plass, M. F. and Tarjan, R. E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas, Inform. Process. Lett. 8(3) (1979), 121–123.

Bryant, R. E.: Graph-based algorithms for Boolean function manipulation, IEEE Trans. Comput., C-35(8) (1986).

Cook, S. A.: The complexity of theorem proving procedures, in Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing, 1971, pp. 151–158.

Van Dalen, D.: Logic and Structure, 3rd edn, Springer-Verlag, Berlin, 1994.

Davis, M., Logemann, M. and Loveland, D.: A machine program for theorem proving, Comm. ACM 5 (1962), 394–397.

Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. ACM 7 (1960), 210–215.

Dowling, W. F. and Gallier, J. H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Logic Programming 1(3) (1984), 267–284.

Dubois, O., Andre, P., Boufkhad, Y. and Carlier, J.: SAT versus UNSAT, in Johnson and Trick [22], pp. 415–436.

Fokkink, W. J.: Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd, in Proceedings of the 5th Conference on Computers in Railways-COMPRAIL'96, Volume I: Railway Systems and Management, Computational Mechanics Publications, 1996, pp. 101–110.

Freeman, J. W.: Improvements to propositional satisfiability search algorithms, Ph.D. Thesis, Department of Computer Science, University of Pennsylvania, USA, 1995.

Gallo, G. and Scutellá, M. G.: Polynomially solvable satisfiability problems, Inform. Process. Lett. 29 (1988), 221–227.

Van Gelder, A. and Okushi, F.: A propositional theorem prover to solve planning and other problems, Technical Report, Computer Science Department, University of California, Santa Cruz, CA, 1998.

Van Gelder, A. and Tsuji, Y. K.: Satisfiability testing with more reasoning and less guessing, in Johnson and Trick [22], pp. 559–586.

Groote, J. F.: Hiding propositional constants in BDDs, Formal Methods in System Design 8 (1996), 91–96.

Groote, J. F., Koorn, J. W. C. and van Vlijmen, S. F. M.: The safety guaranteeing system at station Hoorn-Kersenboogerd (extended abstract), in Proceedings 10th IEEE Conference on Computer Assurance (COMPASS'95), Maryland, 1995, pp. 57–68.

Gu, J.: Local search for the satisfiability (SAT) problem, IEEE Trans. Syst. Man Cybernet. 23(4) (1993), 1108–1129.

Gu, J.: Global optimization for satisfiability (SAT) problem, IEEE Trans. Knowledge Data Engrg. 6(3) (1994), 361–381.

Gu, J., Purdom, P. W., Franco, J. and Wah, B. W.: Algorithms for the satisfiability (SAT) problem: A survey, in D. Du, J. Gu, and P. M. Pardalos (eds.), Satisfiability Problem: Theory and Applications, DIMACS Ser. Discrete Math. and Comput. Sci. 35, Amer. Math. Soc., 1997, pp. 9–151.

Harrison, J.: Stå llmarck's algorithm as a HOL derived rule, in J. von Wright, J. Grundy, and J. Harrison (eds.), Proceedings of TPHOLs'96, Lecture Notes in Comput. Sci. 1125, 1996, pp. 221–234.

Hooker, J. N. and Vinay, V.: Branching rules for satisfiability, J. Automated Reasoning 15(3) (1995), 359–383.

Johnson, D. S. and Trick, M. A. (eds.): Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Ser. Discrete Math. and Comput. Sci. 26, Amer. Math. Soc., 1996.

Krajícek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and its Applications 60, Cambridge University Press, 1996.

Larrabee, T.: Efficient generation of test patterns using Boolean satisfiability, IEEE Trans. Computer-Aided Design 11(1) (1992), 4–15.

VanMaaren, H., Groote, J. F. and Rozema, M.: Verification of propositional formulae by means of convex and concave transforms, Technical Report 95–74, Faculty of Technical Mathematics and Informatics, Delft University of Technology, Delft, The Netherlands, 1995.

Mertens, J.: Verifying the safety guaranteeing system at railway station Heerhugowaard, Master's thesis, University of Utrecht, Utrecht, The Netherlands, 1996.

Mitchell, D., Selman, B. and Levesque, H.: Hard and easy distributions of SAT problems, in Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92), San Jose, CA, 1992, pp. 459–465.

Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. ACM 12 (1965), 23–41.

Selman, B., Levesque, H. and Mitchell, D.: A new method for solving hard satisfiability problems, in Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92), San Jose, CA, 1992, pp. 440–446.

Marques Silva, J. P. and Sakallah, K. A.: Conflict analysis in search algorithms for propositional satisfiability, Technical Report RT/4/96, Cadence European Laboratories, ALGOS, INESC, Lisbon, Portugal, 1996.

Stå llmarck, G.: A proof theoretic concept of tautological hardness, Incomplete manuscript, 1994.

Stå llmarck, G.: System for determining propositional logic theorems by applying values and rules to triplets that are generated from Boolean formula, United States Patent number 5,276,897; Swedish Patent 467 076; European Patent 0 403 454; Canadian Patent 2,018,828, 1994.

Trick, M. A.: Second DIMACS challenge test problems, in Johnson and Trick [22], pp. 653–657.

Tseitin, G. S.: On the complexity of derivation in propositional calculus, Stud. Constructive Math. and Math. Logic 2 (1968), 115–125. Reprinted in J. Siekmann and G. Wrightson (eds.), Automation of Reasoning, Vol. 2, Springer-Verlag, Berlin, 1983.

Urquhart, A.: The complexity of propositional proofs, The Bulletin of Symbolic Logic 1(4) (1995), 425–467.

Warners, J. P. and Van Maaren, H.: A two-phase algorithm for solving a class of hard satisfiability problems, Oper. Res. Lett. 23(3–5) (1999), 81–88.

Widebäck, F.: Stå llmarck's notion of n-saturation, Technical Report NP-K-FW-200, Logikkonsult NP AB, Sweden, 1996.

Wilson, J. M.: Compact normal forms in propositional logic and integer programming formulations, Comput. Oper. Res. 17(3) (1990), 309–314.

Wos, L., Overbeek, R., Lusk, E. and Boyle, J.: Automated Reasoning, McGraw-Hill, 1992.

Zhang, H.: SATO: An efficient propositional solver, in W. McCune (ed.), Automated Deduction-CADE-14, Lecture Notes in Artif. Intell. 1249, Springer, 1997, pp. 272–275.