The propositional formula checker HeerHugo. HeerHugo 0.3 is a propositional theorem prover that tries to prove (large) propositions a contradiction. Typical examples, in the syntax of HeerHugo are p& p (contradiction), p|(q->(abcd<->s)) (satisfiable). The input is put in a file Ain, and the output is put in a file Aout. By adapting the file parameters.h a number of compile time options can be set, such as the maximum number of proposition letters (which has been set to over 150.000.000 for some experiments using an adapted version of HeerHugo). The tool (gzipped tar file) together with an accompanying paper (postscript or pdf) are available. The software can be used free of charge but it comes without any guarantee.

References in zbMATH (referenced in 18 articles )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin: Efficient CNF simplification based on binary implication graphs (2011)
  2. Lonsing, Florian; Biere, Armin: Failed literal detection for QBF (2011)
  3. Peltier, Nicolas: Extended resolution simulates binary decision diagrams (2008)
  4. Eriksson, Lars-Henrik: The GTO toolset and method (2007) ioport
  5. Lynce, Inês; Marques-Silva, João: Efficient data structures for backtrack search SAT solvers (2005)
  6. Ojeda-Aciego, M.; Valverde, A.: tascpl: TAS solver for classical propositional logic (2004)
  7. Okushi, Fumiaki; Van Gelder, Allen: Persistent and quasi-persistent lemmas in propositional model elimination (2004)
  8. Bruni, Renato: Approximating minimal unsatisfiable subformulae by means of adaptive core search (2003)
  9. Bruni, Renato; Sassano, Antonio: A complete adaptive algorithm for propositional satisfiability (2003)
  10. Fiorini, Claudia; Martinelli, Enrico; Massacci, Fabio: How to fake an RSA signature by encoding modular root finding as a SAT problem (2003)
  11. Li, Chu-Min: Equivalent literal propagation in the DLL procedure (2003)
  12. Zantema, Hans; Groote, Jan Friso: Transforming equality logic to propositional logic (2003)
  13. Ayari, Abdelwaheb; Basin, David: QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers (2002)
  14. Niebert, Peter; Mahfoudh, Moez; Asarin, Eugene; Bozga, Marius; Maler, Oded: Verification of timed automata via satisfiability checking (2002)
  15. Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando; Vardi, Moshe Y.: Towards an efficient library for SAT: A manifesto (2001)
  16. Simon, Laurent; Chatalic, Philippe: SatEx: A web-based framework for SAT experimentation (2001)
  17. Groote, Jan Friso; Warners, Joost P.: The propositional formula checker HeerHugo (2000)
  18. Groote, Jan Friso; Warners, Joost P.: The propositional formula checker HeerHugo (2000)