ZRes swMATH ID: 28380 Software Authors: Chatalic, Philippe; Simon, Laurent Description: ZRes: The old Davis-Putnam procedure meets ZBDD. ZRes is a propositional prover based on the original procedure of Davis and Putnam, as opposed to its modified version of Davis, Logeman and Loveland, on which most of the current efficient SAT provers are based. On some highly structured SAT instances, such as the well known Pigeon Hole and Urquhart problems, both proved hard for resolution, ZRFs performs very well and surpasses all classical SAT provers by an order of magnitude. Homepage: https://rd.springer.com/chapter/10.1007/10721959_35 Related Software: Chaff; SATO; MiniSat; HeerHugo; DIMACS; SatEx; MiniMaxSat; CBMC; Jerusat; Alcoa; NQTHM; Sat4j; TestEra; BerkMin; SATzilla; QingTing1; Alloy; UnitWalk; GAP; Lingeling Cited in: 9 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year ZRes: The old Davis-Putnam procedure meets ZBDD. Zbl 0963.68534Chatalic, Philippe; Simon, Laurent 2000 all top 5 Cited by 15 Authors 2 Biere, Armin 2 Chatalic, Philippe 2 Simon, Laurent S. R. 1 Al-Yahya, Tasniem Nasser 1 Eén, Niklas 1 El-bachir Menai, Mohamed 1 Ignatyev, Alexey A. 1 Li, Chumin 1 Markov, Igor L. 1 Minato, Shin-ichi 1 Motter, DoRon B. 1 Plaisted, David Alan 1 Roy, Jarrod A. 1 Semenov, Aleksandr Anatol’evich 1 Zhu, Yunshan Cited in 3 Serials 2 Discrete Applied Mathematics 1 Journal of Computer Science and Technology 1 Annals of Mathematics and Artificial Intelligence Cited in 3 Fields 8 Computer science (68-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year