Modern SAT solvers: fast, neat and underused (2018)

• scala

  45 14,279 9.8 Scala

  Scala 2 compiler and standard library. Bugs at https://github.com/scala/bug; Scala 3 at https://github.com/scala/scala3

  

Compiling Scala without a SAT solver is probably too difficult.

The CNF Converter is a gem.

https://github.com/scala/scala/blob/v2.13.5/src/compiler/sca...

• sturm

  2 9 10.0 Python

  Simpleminded terminal interface

FWIW, here's a little console-mode puzzle game of SAT problems, if you want to solve some manually. The "board" is not exactly like the example table in the post, since that one was for Sudoku in particular. This grid represents variables as rows and clauses as columns.

https://github.com/darius/sturm/blob/master/satgame.py (Python 2)

• InfluxDB

  www.influxdata.com featured

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• clingo

  3 586 7.9 C++

  🤔 A grounder and solver for logic programs.

  

Love this article and the push to build awareness of what modern SAT solvers can do.

The thing it misses, though, is that there are higher level abstractions that are far more accessible than SAT. If I were teaching a course on this, I would start with either Answer Set Programming or Satisfiability Modulo Theories (SMT). The most widely used solvers for those are clingo [0] and Z3 [1]:

With ASP, you write in a much clearer Prolog-like syntax that does not require nearly as much encoding effort as your typical SAT problem. Z3 is similar -- you can code up problems in a simple Python API, or write them in the smtlib language.

Both of these make it easy to add various types of optimization, constraints, etc. to your problem, and they're much better as modeling languages than straight SAT. Underneath, they have solvers that leverage all the modern CDCL tricks.

We wrote up a paper [2] on how to formulate a modern dependency solver in ASP; it's helped tremendously for adding new types of features like options, variants, and complex compiler/arch dependencies to Spack [3]. You could not get good solutions to some of these problems without a capable and expressive solver.

[0] https://github.com/potassco/clingo

• z3

  28 9,754 9.8 C++

  The Z3 Theorem Prover

  

• spack

  52 3,985 10.0 Python

  A flexible package manager that supports multiple versions, configurations, platforms, and compilers.

  

• pub

  21 1,030 9.2 Dart

  The pub command line tool

  

• Decider

  2 145 0.0 C#

  An Open Source .Net Constraint Programming Solver (by lifebeyondfife)

Plug for my Constraint Solver if anyone wants a simple example https://github.com/lifebeyondfife/Decider

• SaaSHub

  www.saashub.com featured

  SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

  

Suggest a related project