gbury/msat

A modular sat/smt solver with proof output.

msat's Issues

use non generative api

replace generative functors by mere functors (or modules), and provide a type t which wraps the state.

pros:

• state is more explicit
• globals are now embedded in t and can be gc'd
• more customizable: val create: ?size:int -> ?callback:… -> unit -> t
• easier to copy/(de)serialize if need be
• easier to integrate in other type t-based APIs
• more convenient (no local module necessary)

cons:

• change API

assertion failure

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

design clean API for theories

instead of exposing dirty St:

• simplify the internals by removing Solver_types.mli
• have a submodule for each type in Solver_types.ml
• expose only a carefully chosen part of each module outside of Msat

ability to push decisions from the theory

would be useful for the theory to be able to make boolean decisions, for z3-style theory combination

assert failure

Fatal error: exception File "src/core/internal.ml", line 676, characters 16-22: Assertion failed

• msat at 66707b5,
• smbc at 001b56ebb46.

run ./smbc.native --debug 1 examples/long_rev_sum5.lisp --max-depth 1010
(around 6s environ)

vec.get error

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

Use reflexivity in Coq proofs

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).

invalid_argument

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

requires zarith?

I tried to install msat using opam-deducteam, and it failed with

ocamlfind: Package `zarith' not found

is it a missing dependency?

access literals' decision level from theory

function to add a literal

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.

perf: phase saving

• use a bool flag in the variable to save last phase
• use false by default (corresponds to this flag being cleared)

How to get non-deterministic solutions?

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 :).

bug

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

make theory able to set default polarity of vars

perf regression on 0.9

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 -)?

DRAT proof output

Setup Github Actions CI

This repo used to use Travis CI, but since the free service ended, there is no CI anymore.

Improve performances

Goal

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:

• finely tune the flambda options of the compiler to fully profit from the optimizations available
• identify bottlenecks in the code using the spacetime profiler, and propose modifications to the code

Testing

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.

Current status

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.