PicoSAT essentials. We describe and evaluate optimized compact data structures for watching literals. Experiments with our SAT solver PicoSAT show that this low-level optimization not only saves memory, but also turns out to speed up the SAT solver considerably. We also discuss how to store proof traces compactly in memory and further unique features of PicoSAT including an aggressive restart schedule.

References in zbMATH (referenced in 55 articles , 1 standard article )

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

1 2 3 next

  1. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  2. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  3. Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
  4. Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Checking EMTLK properties of timed interpreted systems via bounded model checking (2016)
  5. Biere, Armin; Fröhlich, Andreas: Evaluating CDCL variable scoring schemes (2015)
  6. Heule, Marijn J.H.; Hunt, Warren A.jun.; Wetzler, Nathan: Expressing symmetry breaking in DRAT proofs (2015)
  7. Klimoš, Miroslav; Kučera, Antonín: Cobra: a tool for solving general deductive games (2015)
  8. Achá, Roberto Asín; Nieuwenhuis, Robert: Curriculum-based course timetabling with SAT and MaxSAT (2014)
  9. Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter: On the van der Waerden numbers $\mathrmw(2; 3, t)$ (2014)
  10. Belov, Anton; Janota, Mikoláš; Lynce, In^es; Marques-Silva, Joao: Algorithms for computing minimal equivalent subformulas (2014)
  11. Belov, Anton; Marques-Silva, Joao: MUSer2: an efficient MUS extractor (2014)
  12. Creus, Carles; Godoy, Guillem: Automatic evaluation of context-free grammars (system description) (2014)
  13. Goldberg, Eugene; Manolios, Panagiotis: Quantifier elimination by dependency sequents (2014)
  14. Ansótegui, Carlos; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (2013)
  15. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013)
  16. Belov, Anton; Manthey, Norbert; Marques-Silva, Joao: Parallel MUS extraction (2013)
  17. Belov, Anton; Morgado, António; Marques-Silva, Joao: SAT-based preprocessing for maxsat (2013)
  18. Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao: Iterative and core-guided maxsat solving: a survey and assessment (2013)
  19. Wetzler, Nathan; Heule, Marijn J.H.; Hunt, Warren A.Jr.: Mechanical verification of SAT refutations with extended resolution (2013)
  20. Zhou, Min; He, Fei; Wang, Bow-Yaw; Gu, Ming; Sun, Jiaguang: A unified framework for DPLL(T) + certificates (2013)

1 2 3 next

Further publications can be found at: http://fmv.jku.at/papers/index.html