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.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
- Ignatiev, Alexey; Semenov, Alexander: DPLL+ROBDD derivation applied to inversion of some cryptographic functions (2011)
- Minato, Shin-ichi: (\pi)DD: a new decision diagram for efficient problem solving in permutation space (2011)
- Eén, Niklas; Biere, Armin: Effective preprocessing in SAT through variable and clause elimination (2005)
- Motter, DoRon B.; Roy, Jarrod A.; Markov, Igor L.: Resolution cannot polynomially simulate compressed-BFS (2005)
- Li, Chu-Min: Equivalent literal propagation in the DLL procedure (2003)
- Plaisted, David A.; Biere, Armin; Zhu, Yunshan: A satisfiability procedure for quantified Boolean formulae (2003)
- Simon, Laurent; Chatalic, Philippe: SatEx: A web-based framework for SAT experimentation (2001)
- Chatalic, Philippe; Simon, Laurent: ZRes: The old Davis-Putnam procedure meets ZBDD (2000)