Coder Social home page Coder Social logo

laplacekorea / toysolver Goto Github PK

View Code? Open in Web Editor NEW

This project forked from msakai/toysolver

0.0 1.0 0.0 7.09 MB

My sandbox for experimenting with solver algorithms.

License: Other

Shell 0.58% Ruby 0.09% C++ 0.22% C 0.95% Haskell 98.15% Dockerfile 0.01%

toysolver's Introduction

toysolver

License Join the chat at https://gitter.im/msakai/toysolver

Hackage: Hackage Hackage Deps Hackage CI

Dev: Build Status (AppVeyor) Build Status (GitHub Actions) Coverage Status

It provides solver implementations of various problems including SAT, SMT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.

In particular it contains moderately-fast pure-Haskell SAT solver 'toysat'.

Installation

See INSTALL.md.

Usage

This package includes several commands.

toysolver

Arithmetic solver for the following problems:

  • Mixed Integer Liner Programming (MILP or MIP)
  • Boolean SATisfiability problem (SAT)
  • PB
    • Pseudo Boolean Satisfaction (PBS)
    • Pseudo Boolean Optimization (PBO)
    • Weighted Boolean Optimization (WBO)
  • Max-SAT families
    • Max-SAT
    • Partial Max-SAT
    • Weighted Max-SAT
    • Weighted Partial Max-SAT
  • Real Closed Field

Usage:

toysolver [OPTION...] [file.lp|file.mps]
toysolver --lp [OPTION...] [file.lp|file.mps]
toysolver --sat [OPTION...] [file.cnf]
toysolver --pb [OPTION...] [file.opb]
toysolver --wbo [OPTION...] [file.wbo]
toysolver --maxsat [OPTION...] [file.cnf|file.wcnf]

-h  --help           show help
-v  --version        show version number
    --solver=SOLVER  mip (default), omega-test, cooper, cad, old-mip, ct

toysat

SAT-based solver for the following problems:

  • SAT
    • Boolean SATisfiability problem (SAT)
    • Minimally Unsatisfiable Subset (MUS)
    • Group-Oriented MUS (GMUS)
  • PB
    • Pseudo Boolean Satisfaction (PBS)
    • Pseudo Boolean Optimization (PBO)
    • Weighted Boolean Optimization (WBO)
  • Max-SAT families
    • Max-SAT
    • Partial Max-SAT
    • Weighted Max-SAT
    • Weighted Partial Max-SAT
  • Integer Programming (all variables must be bounded)

Usage:

toysat [file.cnf|-]
toysat --sat [file.cnf|-]
toysat --mus [file.gcnf|file.cnf|-]
toysat --pb [file.opb|-]
toysat --wbo [file.wbo|-]
toysat --maxsat [file.cnf|file.wcnf|-]
toysat --lp [file.lp|file.mps|-]

PB'12 competition result:

  • toysat placed 2nd in PARTIAL-BIGINT-LIN and SOFT-BIGINT-LIN categories
  • toysat placed 4th in PARTIAL-SMALLINT-LIN and SOFT-SMALLINT-LIN categories
  • toysat placed 8th in OPT-BIGINT-LIN category

toysmt

SMT solver based on toysat.

Usage:

toysmt [file.smt2]

Currently only QF_UF, QF_RDL, QF_LRA, QF_UFRDL and QF_UFLRA logic are supported.

toyfmf

SAT-based finite model finder for first order logic (FOL).

Usage:

toyfmf [file.tptp] [size]

toyconvert

Converter between various problem files.

Usage:

toyconvert -o [outputfile] [inputfile]

Supported formats:

  • Input formats: .cnf .wcnf .opb .wbo .gcnf .lp .mps
  • Output formats: .cnf .wcnf .opb .wbo .lsp .lp .mps .smp .smt2 .ys

Bindings

Spin-off projects and packages

toysolver's People

Contributors

msakai avatar hsenag avatar katrinleinweber avatar gitter-badger avatar

Watchers

 avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.