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.68534
Chatalic, Philippe; Simon, Laurent

Citations by Year