kcnfs is a dpll based solver. kcnfs integrates a branching variable heuristic devoted essentially to prove the unsatisfiability of random k-sat formulae and which has been inspired by recent statistical physics work. This heuristic waspresented in [DD01] and generalized to solve k-sat formulae with a renormalization strategy in[DD03]. The local techniques called ”picking” first described in [DD01] were implemented in kcnfs.
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer (2016)
- Kullmann, Oliver: Present and future of practical SAT solving (2008)
- Heule, Marijn; van Maaren, Hans: Effective incorporation of double look-ahead procedures (2007)
- Dequen, Gilles; Dubois, Olivier: An efficient approach to solving random (k)-SAT problems (2006)
- Armando, Alessandro; Castellini, Claudio; Giunchiglia, Enrico; Maratea, Marco: The SAT-based approach to separation logic (2005)
- Darras, S.; Dequen, G.; Devendeville, L.; Mazure, B.; Ostrowski, R.; Saïs, L.: Using Boolean constraint propagation for sub-clauses deduction (2005)
- Dequen, Gilles; Dubois, Olivier: \textitkcnfs: An efficient solver for random (k)-SAT formulae (2004)
- Nudelman, Eugene; Leyton-Brown, Kevin; Hoos, Holger H.; Devkar, Alex; Shoham, Yoav: Understanding random SAT: Beyond the clauses-to-variables ratio (2004)