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 43 articles )

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

1 2 3 next

  1. Feng, Yu; Martins, Ruben; Wang, Yuepeng; Dillig, Isil; Reps, Thomas W.: Component-based synthesis for complex apis (2017)
  2. 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 \ssfAProVE (2017)
  3. Hutter, Frank; Lindauer, Marius; Balint, Adrian; Bayless, Sam; Hoos, Holger; Leyton-Brown, Kevin: The configurable SAT solver challenge (CSSC) (2017)
  4. Janhunen, Tomi; Gebser, Martin; Rintanen, Jussi; Nyman, Henrik; Pensar, Johan; Corander, Jukka: Learning discrete decomposable graphical models via constraint optimization (2017)
  5. Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc: CNFgen: a generator of crafted benchmarks (2017)
  6. Luo, Chuan; Cai, Shaowei; Su, Kaile; Huang, Wenxuan: CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability (2017)
  7. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  8. Ansótegui, Carlos; Gabàs, Joel; Malitsky, Yuri; Sellmann, Meinolf: MaxSAT by improved instance-specific algorithm configuration (2016)
  9. Cai, Shaowei; Luo, Chuan; Lin, Jinkun; Su, Kaile: New local search methods for partial MaxSAT (2016)
  10. Cohen, D.; Crampton, J.; Gagarin, A.; Gutin, G.; Jones, M.: Algorithms for the workflow satisfiability problem engineered for counting constraints (2016)
  11. Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao: Quantified maximum satisfiability (2016)
  12. Kuželka, Ondřej; Davis, Jesse; Schockaert, Steven: Constructing Markov logic networks from first-order default rules (2016)
  13. Zohar, Yoni; Zamansky, Anna: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi (2016)
  14. Karapetyan, Daniel; Gagarin, Andrei; Gutin, Gregory: Pattern backtracking algorithm for the workflow satisfiability problem with user-independent constraints (2015)
  15. Rahwan, Talal; Michalak, Tomasz P.; Wooldridge, Michael; Jennings, Nicholas R.: Coalition structure generation: a survey (2015)
  16. Artigues, Christian; Hebrard, Emmanuel; Mayer-Eichberger, Valentin; Siala, Mohamed; Walsh, Toby: SAT and hybrid models of the car sequencing problem (2014)
  17. Martins, Ruben; Manquinho, Vasco; Lynce, In^es: Open-WBO: a modular MaxSAT solver (2014)
  18. Soh, Takehide; Le Berre, Daniel; Roussel, Stéphanie; Banbara, Mutsunori; Tamura, Naoyuki: Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem (2014)
  19. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  20. Bofill, Miquel; Busquets, Dídac; Muñoz, Víctor; Villaret, Mateu: Reformulation based MaxSat robustness (2013)

1 2 3 next