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

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Scout Monitoring - Free Django app performance insights with Scout Monitoring
Get Scout setup in minutes, and let us sweat the small stuff. A couple lines in settings.py is all you need to start monitoring your apps. Sign up for our free tier today.
www.scoutapm.com
featured
InfluxDB - 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.
www.influxdata.com
featured
  • scala

    Scala 2 compiler and standard library. Scala 2 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...

  • Scout Monitoring

    Free Django app performance insights with Scout Monitoring. Get Scout setup in minutes, and let us sweat the small stuff. A couple lines in settings.py is all you need to start monitoring your apps. Sign up for our free tier today.

    Scout Monitoring logo
  • sturm

    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)

  • clingo

    🤔 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

    The Z3 Theorem Prover

  • spack

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

  • pub

    The pub command line tool

  • Decider

    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

  • InfluxDB

    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.

    InfluxDB logo
NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts

  • Autodafe: "freeing your freeing your project from the clammy grip of autotools."

    4 projects | news.ycombinator.com | 6 Apr 2024
  • "xAI will open source Grok"

    3 projects | news.ycombinator.com | 11 Mar 2024
  • FreeBSD has a(nother) new C compiler: Intel oneAPI DPC++/C++

    2 projects | news.ycombinator.com | 7 Mar 2024
  • The Curious Case of MD5

    4 projects | news.ycombinator.com | 3 Jan 2024
  • Apache Spark VS quix-streams - a user suggested alternative

    2 projects | 7 Dec 2023