Displaying 1 to 11 from 11 results

gophersat - gophersat, a SAT solver in Go

  •    Go

This is Gophersat, a SAT and pseudo-boolean solver written purely in Go. Gophersat was developed by the CRIL (Centre de Recherche en Informatique de Lens) at the Artois University & CNRS. It is released under the MIT license. Gophersat is rather efficient, i.e on typical SAT benchmarks it runs about 2 to 5 times slower than top-level solvers (namely, glucose or minisat) from which it is strongly inspired. It can also solve MAXSAT problems, and pseudo-boolean decision and optimization problems. Gophersat's last stable version is version 1.1. It includes a new, more efficient core solver for pure SAT problems and a package for dealing with MAXSAT problems. It also includes a new API for optimization and model counting, where new models are written to channels as soon as they are found.

go-sat - SAT solver written in Go (golang).

  •    Go

go-sat is a pure Go library for solving Boolean satisfiability problems (SAT).Solving SAT problems is at the core of a number of more difficult higher level problems. From hardware/software verification, scheduling constraints, version resolution, etc. many problems are reduced fully or partially to a SAT problem.

go-z3 - Go (golang) bindings to the Z3 SMT Solver

  •    Go

go-z3 provides bindings to Z3, a theorem prover out of Microsoft Research. Z3 is a state-of-the-art SMT Solver.This library provides bindings via cgo directly to Z3.

haskell-picosat - Haskell bindings for PicoSAT solver

  •    C

haskell-picosat are Haskell bindings to the PicoSAT solver, written in C. It reads in clauses in CNF ( Conjunctive-Normal Form ) and returns a solution which satisfies the clauses. The most notable distinction of this binding is that the SAT solver library is included with the cabal package so you shouldn't need to install anything but this package to get going. It's also notably faster than a pure Haskell solution at solving very large constraint problems.

picologic - Logic expressions for PicoSAT solver

  •    Haskell

Picologic is a lightweight library for working with symbolic logic expressions. It is built against the picosat Haskell library which bundles the SAT solver with the Haskell package so no external solver or dependencies are necessary. Picologic provides the logic expressions, parser and normal form conversion functions to express the logic expressions more naturally and then feed them to the SAT solver.

gapt - GAPT: General Architecture for Proof Theory

  •    Scala

GAPT is a proof theory framework developed primarily at the Vienna University of Technology. GAPT contains data structures, algorithms, parsers and other components common in proof theory and automated deduction. In contrast to automated and interactive theorem provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further processing of proofs. You can also use Prover9, Vampire, EProver, and lots of other provers instead of the built-in Escargot prover, if you have them installed. There are many more examples in the user manual, and you can look into the API documentation for reference as well.

yices2 - The Yices SMT Solver

  •    SMT

Yices 2 is a solver for Satisfiability Modulo Theories (SMT) problems. Yices 2 can process input written in the SMT-LIB language, or in Yices' own specification language. We also provide a C API and Python language bindings. This repository includes the source of Yices 2, documentation, tests, and examples.

MK85 - toy-level, simple SMT solver

  •    C

It's very early sneak preview. It supports only bools and bitvecs. No integers, let alone reals and arrays and tuples and whatnot. Its complexity is comparable to simple LISP interpreter. However, it can serve as education tool (hopefully). This is also my playground.

gini - A fast SAT solver

  •    Go

The Gini sat solver is a fast, clean SAT solver written in Go. It is to our knowledge the first ever performant pure-Go SAT solver made available. This solver is fully open source, originally developped at IRI France.

mSAT - A modular sat/smt solver with proof output.

  •    OCaml

MSAT is an OCaml library that features a modular SAT-solver and some extensions (including SMT), derived from Alt-Ergo Zero. This program is distributed under the Apache Software License version 2.0. See the enclosed file LICENSE.