Sat4j

The Sat4j library, release 2.2 system description. Sat4j is a java library for solving boolean satisfaction and optimization problems. It can solve SAT, MAXSAT, Pseudo-Boolean, Minimally Unsatisfiable Subset (MUS) problems. Being in Java, the promise is not to be the fastest one to solve those problems (a SAT solver in Java is about 3.25 times slower than its counterpart in C++), but to be full featured, robust, user friendly, and to follow Java design guidelines and code conventions (checked using static analysis of the source code). The library is designed for flexibility, by using heavily the decorator and strategy design patterns. Furthermore, Sat4j is open source, under the dual business friendly Eclipse Public License and academic friendly GNU LGPL license.


References in zbMATH (referenced in 70 articles )

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

1 2 3 4 next

  1. Rocha, Thiago Alves; Martins, Ana Teresa; Ferreira, Francicleber Martins: Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games (2020)
  2. Showkatbakhsh, Mehrdad; Shoukry, Yasser; Diggavi, Suhas N.; Tabuada, Paulo: Securing state reconstruction under sensor and actuator attacks: theory and design (2020)
  3. Demirović, Emir; Musliu, Nysret; Winter, Felix: Modeling and solving staff scheduling with partial weighted maxSAT (2019)
  4. Liao, Xiaojuan; Koshimura, Miyuki; Nomoto, Kazuki; Ueda, Suguru; Sakurai, Yuko; Yokoo, Makoto: Improved WPM encoding for coalition structure generation under MC-nets (2019)
  5. Varshosaz, Mahsa; Luthmann, Lars; Mohr, Paul; Lochau, Malte; Mousavi, Mohammad Reza: Modal transition system encoding of featured transition systems (2019)
  6. Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi: (N)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT (2019)
  7. Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil: Understanding cutting planes for QBFs (2018)
  8. Lagniez, Jean-Marie; Le Berre, Daniel; de Lima, Tiago; Montmirail, Valentin: An assumption-based approach for solving the Minimal S5-Satisfiability problem (2018)
  9. Nadel, Alexander: Solving MaxSAT with bit-vector optimization (2018)
  10. Cohen, D.; Crampton, J.; Gutin, G.; Wahlström, M.: Parameterized complexity of the workflow satisfiability problem (2017)
  11. Demirović, Emir; Musliu, Nysret: maxSAT-based large neighborhood search for high school timetabling (2017)
  12. Feng, Yu; Martins, Ruben; Wang, Yuepeng; Dillig, Isil; Reps, Thomas W.: Component-based synthesis for complex APIs (2017)
  13. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \textsfAProVE (2017)
  14. Hutter, Frank; Lindauer, Marius; Balint, Adrian; Bayless, Sam; Hoos, Holger; Leyton-Brown, Kevin: The configurable SAT solver challenge (CSSC) (2017)
  15. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: On tackling the limits of resolution in SAT solving (2017)
  16. Janhunen, Tomi; Gebser, Martin; Rintanen, Jussi; Nyman, Henrik; Pensar, Johan; Corander, Jukka: Learning discrete decomposable graphical models via constraint optimization (2017)
  17. Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc: CNFgen: a generator of crafted benchmarks (2017)
  18. Lauria, Massimo; Nordström, Jakob: Graph colouring is hard for algorithms based on Hilbert’s Nullstellensatz and Gröbner bases (2017)
  19. Luo, Chuan; Cai, Shaowei; Su, Kaile; Huang, Wenxuan: CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability (2017)
  20. Terra-Neves, Miguel; Lynce, Inês; Manquinho, Vasco: Introducing Pareto minimal correction subsets (2017)

1 2 3 4 next