PrecoSAT uses an MIT style license. In essence, you can use and modify the sources as you like provided that you acknowledge the origin of the software in the source code. More details can be found in the LICENSE file that comes with the sources. There is no warranty. Background: The ideas behind PrecoSAT are partially described in the system description for the SAT’09 SAT Competition. SAT is the classical NP complete problem of searching for a satisfying assignment of a propositional formula in conjunctive normal form (CNF). The Handbook of Satisfiability gives an excellent overview of theoretical and practical aspects for the field. Further information on SAT can be found at or We also have some recent papers on SAT mostly focusing on practical SAT solving. On our software page you find earlier SAT solvers and related tools by our group.

References in zbMATH (referenced in 18 articles )

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

  1. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  2. Ngoko, Yanik; Cérin, Christophe; Trystram, Denis: Solving SAT in a distributed cloud: a portfolio approach (2019)
  3. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  4. Wickerson, John; Batty, Mark; Sorensen, Tyler; Constantinides, George A.: Automatically comparing memory consistency models (2017)
  5. Liang, Jia Hui; Ganesh, Vijay; Poupart, Pascal; Czarnecki, Krzysztof: Learning rate based branching heuristic for SAT solvers (2016)
  6. Philipp, Tobias: An expressive model for instance decomposition based parallel SAT solvers (2015)
  7. Belov, Anton; Morgado, António; Marques-Silva, Joao: SAT-based preprocessing for MaxSAT (2013)
  8. Fagerberg, Rolf; Flamm, Christoph; Merkle, Daniel; Peters, Philipp; Stadler, Peter F.: On the complexity of reconstructing chemical reaction networks (2013)
  9. Manthey, Norbert; Philipp, Tobias; Wernhard, Christoph: Soundness of inprocessing in clause sharing SAT solvers (2013)
  10. Morawiecki, Paweł; Srebrny, Marian: A SAT-based preimage analysis of reduced \textscKeccakhash functions (2013)
  11. Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric; Mayer-Eichberger, Valentin: A new look at BDDs for pseudo-Boolean constraints (2012)
  12. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
  13. Järvisalo, Matti; Kaski, Petteri; Koivisto, Mikko; Korhonen, Janne H.: Finding efficient circuits for ensemble computation (2012)
  14. Martins, Ruben; Manquinho, Vasco; Lynce, Inês: An overview of parallel SAT solving (2012)
  15. Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric: Cardinality networks: a theoretical and empirical study (2011)
  16. Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin: Efficient CNF simplification based on binary implication graphs (2011)
  17. Ignatiev, Alexey; Semenov, Alexander: DPLL+ROBDD derivation applied to inversion of some cryptographic functions (2011)
  18. Hyvärinen, Antti E. J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning SAT instances for distributed solving (2010)

Further publications can be found at: