Finite domain enumerator. This is a finite domain CSP solver, rather limited in what it can do. Don’t expect it to deal effectively with anything numerical, though it can knock off small problems reasonably quickly. The nice feature (say I) is the input language which is first order logic thinly disguised. Earlier versions of this came with some documentation. This one comes with the injunction to use the Force (read the source). Also read the README that comes with it.

References in zbMATH (referenced in 40 articles )

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

1 2 next

  1. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  2. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  3. Gajdoš, Petr; Kuřil, Martin: Ordered semigroups of size at most 7 and linearly ordered semigroups of size at most 10. (2014)
  4. Shah, Muhammad; Gretton, Charles; Sorge, Volker: Enumerating AG-groups with a study of Smaradache AG-groups. (2011)
  5. Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
  6. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)
  7. Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare: Computing finite models by reduction to function-free clause logic (2009)
  8. Peltier, Nicolas: Constructing infinite models represented by tree automata (2009)
  9. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automating algebraic specifications of non-freely generated data types (2008)
  10. Peltier, Nicolas: Automated model building: From finite to infinite models (2008)
  11. Audemard, Gilles; Benhamou, Belaïd; Henocque, Laurent: Predicting and detecting symmetries in FOL finite model search (2006)
  12. Huang, Zhuo; Zhang, Jian: Generating SAT instances from first-order formulas (2005)
  13. Konrad, Karsten: Model generation for natural language interpretation and analysis. (2004)
  14. Zhang, Jian; Zhang, Hantao: Extending finite model searching with congruence closure computation (2004)
  15. Peltier, Nicolas: A calculus combining resolution and enumeration for building finite models (2003)
  16. Peltier, Nicolas: Extracting models from clause sets saturated under semantic refinements of the resolution rule. (2003)
  17. Choi, Seungyeob: Towards semantic goal-directed forward reasoning in resolution (2002)
  18. Dubois, Olivier; Dequen, Gilles: The non-existence of (3,1,2)-conjugate orthogonal idempotent Latin square of order 10 (2001)
  19. Letz, Reinhold; Stenz, Gernot: Proof and model generation with disconnection tableaux (2001)
  20. Bry, François; Yahya, Adnan: Positive unit hyperresolution tableaux and their application to minimal model generation (2000)

1 2 next