gbury / msat Goto Github PK
View Code? Open in Web Editor NEWA modular sat/smt solver with proof output.
Home Page: https://gbury.github.io/mSAT/
License: Apache License 2.0
A modular sat/smt solver with proof output.
Home Page: https://gbury.github.io/mSAT/
License: Apache License 2.0
smbc @ f36a3af4bbd1e76bc85b00957224eb7ee9d1db58
msat @ 03dd2f9
OCaml 4.03
doesn't work but should: ./smbc.native --debug 1 -t 60 --check examples/sorted.lisp
almost similar: ./smbc.native --debug 1 -t 60 --check examples/sorted.lisp --depth-step 2
note: this works well ./smbc.native --debug 1 -t 60 --check examples/ty_infer.lisp
replace generative functors by mere functors (or modules), and provide a type t
which wraps the state.
pros:
t
and can be gc'dval create: ?size:int -> ?callback:โฆ -> unit -> t
type t
-based APIscons:
mSAT currently compares quite unfavorably with other available sat solvers (see https://github.com/Gbury/sat-bench/blob/master/problems/pigeon/results ). It would be interesting to study how to improve performances either by:
Test files can be found under the tests
directory. Additionally, the https://github.com/Gbury/sat-bench is meant to provide interesting problems on which to test and benchmark the various sat solvers, including mSAT. The problems in the repository should provide good runs on which to profile mSAT.
The profile
branch contains the necessary instrumentation using the landmarks library. A simple make bench
in that branch should compile the instrumented binary, and execute it on a reasonably sized problem, which takes about 10s currently.
The current bottleneck is, unsurprisingly, the propagation of atoms. One point of particular interest is why the propagate_in_clause
function makes up such a small proportion of the propagate_atom
function, and similarly, how the time spent in propagate_in_clause
is distributed. In these two cases, the automatic instrumentation of landmarks seems to not be enough to have precise enough information.
with zipperposition e0d2d2e4ce4e695eb044393642d53fcf6318235f :
./zipperposition.native examples/ind/tree3_easy.zf -bt
File "src/core/res.ml", line 203, characters 6-12: Assertion failed
Raised at file "src/core/res.ml" (inlined), line 203, characters 6-47
Called from file "src/core/res.ml", line 261, characters 19-27
Called from file "src/prover/sat_solver.ml", line 227, characters 4-19
Called from file "src/core/CCFun.ml" (inlined), line 18, characters 22-27
Called from file "src/prover_calculi/avatar.ml", line 240, characters 19-73
Called from file "list.ml", line 82, characters 20-23
Called from file "src/prover_calculi/avatar.ml", line 240, characters 10-87
Called from file "src/prover/simplM.ml", line 24, characters 19-22
Called from file "src/prover/simplM.ml", line 24, characters 19-22
Called from file "src/prover/simplM.ml", line 24, characters 19-22
Called from file "src/prover/simplM.ml", line 24, characters 19-22
Called from file "src/prover/env.ml", line 410, characters 18-21
Called from file "src/prover/simplM.ml", line 24, characters 19-22
Called from file "src/prover/env.ml", line 553, characters 10-171
Called from file "src/prover/env.ml", line 410, characters 18-21
Called from file "src/prover/env.ml", line 569, characters 28-43
Called from file "set.ml", line 344, characters 34-55
Called from file "set.ml", line 344, characters 39-54
Called from file "set.ml", line 344, characters 39-54
Called from file "src/prover/env.ml", line 567, characters 6-746
Called from file "src/prover/saturate.ml", line 131, characters 55-78
Called from file "src/prover/saturate.ml", line 185, characters 23-56
Called from file "src/prover_phases/phases_impl.ml", line 301, characters 11-63
Called from file "src/prover_phases/phases.ml", line 116, characters 8-12
Called from file "src/prover_phases/phases.ml", line 116, characters 8-12
Called from file "src/prover_phases/phases.ml", line 116, characters 8-12
Called from file "src/prover_phases/phases.ml", line 116, characters 8-12
Called from file "src/prover_phases/phases.ml", line 208, characters 4-8
using https://github.com/c-cube/sidekick at commit 0b283a384d4f276e2128c1eeb0817b7f8cf17636 the following error is raised within msat:
./sidekick tests/sat/typed_v3l60005.cvc.smt2 --bt
invalid argument:
vec.get
Raised at file "pervasives.ml", line 33, characters 20-45
Called from file "src/core/Vec.ml" (inlined), line 54, characters 29-50
Called from file "src/core/Internal.ml", line 1413, characters 16-40
Called from file "src/core/Internal.ml", line 1503, characters 13-29
Called from file "src/core/Internal.ml", line 1562, characters 10-40
Called from file "src/core/Internal.ml", line 1578, characters 6-22
Called from file "src/core/Internal.ml" (inlined), line 1582, characters 50-67
Called from file "src/core/Internal.ml", line 2035, characters 16-32
Called from file "src/core/Internal.ml", line 2162, characters 6-15
Called from file "src/msat-solver/Sidekick_msat_solver.ml", line 607, characters 12-55
Called from file "src/smtlib/Process.ml", line 155, characters 4-44
Called from file "src/smtlib/Process.ml", line 229, characters 6-130
Called from file "src/core/CCResult.ml", line 239, characters 22-30
Called from file "list.ml", line 100, characters 12-15
Called from file "src/core/CCResult.ml", line 238, characters 4-125
Called from file "src/main/main.ml", line 184, characters 15-21
would be useful for the theory to be able to make boolean decisions, for z3-style theory combination
on pigeon/hole9.cnf it's quite clear.
possibly caused by the bitfield for polarity saving that might be erased when we clear the whole bitfield (even though the default polarity might be +, not -)?
instead of exposing dirty St
:
Solver_types.mli
Solver_types.ml
would be nice to have add_lit: lit -> unit
that forces the solver to decide on this literal, even if there is no constraint on it yet.
with smbc @ 71faccb8e0607c4e05c83ba1041b16be45abd797
./smbc.native --debug 5 --check examples/rev.lisp --depth-step 1 --backtrace
I get
Fatal error: exception Invalid_argument("Sparse_vec.set")
Raised at file "pervasives.ml", line 31, characters 25-45
Called from file "src/util/sparse_vec.ml", line 64, characters 29-57
Called from file "src/core/internal.ml", line 218, characters 6-43
Called from file "src/core/internal.ml", line 420, characters 12-47
Called from file "src/core/internal.ml", line 1145, characters 6-33
Called from file "src/Solver.ml", line 2810, characters 18-41
Called from file "src/smbc.ml", line 55, characters 12-51
Called from file "src/smbc.ml", line 165, characters 2-19
I want to use mSAT to solve (a lot of) quite small CNFs (~40 variables), but I want to get non-deterministic solutions (e.g. a uniform pick from the set of solutions). Could I (easily) do that with this library? I appreciate all suggestions :).
I tried to install msat using opam-deducteam, and it failed with
ocamlfind: Package `zarith' not found
is it a missing dependency?
Fatal error: exception File "src/core/internal.ml", line 676, characters 16-22: Assertion failed
run ./smbc.native --debug 1 examples/long_rev_sum5.lisp --max-depth 1010
(around 6s environ)
false
by default (corresponds to this flag being cleared)Currently coq proof can be quite slow (and even fail to check within reasonable time/memory).
One solution would be to change the structure of coq output from a srie of tactics to the following: write a reflexive function which would compute on a custom data structure (such as a list of resolutions).
This repo used to use Travis CI, but since the free service ended, there is no CI anymore.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.