niklasso/minisat

A minimalistic and high-performance SAT solver

minisat's Issues

Compiling problem when using API with newer g++ version

My project that uses MiniSat did not compile anymore after
updating from Ubuntu 15.10 to 16.10
The following error message was shown:

/home/patrick/uni/SEA/libs/minisat/mtl/Map.h:32:99: error: missing template arguments before ‘(’ token
 late<class K> struct Hash  { uint32_t operator()(const K& k)               const { return hash(k);  } };
                                                                                               ^

and

/home/patrick/uni/SEA/libs/minisat/mtl/Map.h: In member function ‘uint32_t Minisat::DeepHash<K>::operator()(const K*) const’:
/home/patrick/uni/SEA/libs/minisat/mtl/Map.h:35:103: error: missing template arguments before ‘(’ token
 class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };

I could only fix it by replacing those lines as described in the following commit:
see changes
I applied the changes after i compiled MiniSAT, but before I compiled my own tool that includes "minisat/core/Solver.h". That way everything works again, but I'm not sure if that's really the way to resolve the problem..

I am using CMake to link everything together

SET_SOURCE_FILES_PROPERTIES(MiniSatApi.cpp PROPERTIES COMPILE_FLAGS "${COMPILE_FLAGS} -Wno-parentheses -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS")

Before upgrading Ubuntu everything worked just fine.

g++ version:

$ g++ -v
Using built-in specs.
COLLECT_GCC=g++
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/6/lto-wrapper
Target: x86_64-linux-gnu
Configured with: ../src/configure -v --with-pkgversion='Ubuntu 6.2.0-5ubuntu12' --with-bugurl=file:///usr/share/doc/gcc-6/README.Bugs --enable-languages=c,ada,c++,java,go,d,fortran,objc,obj-c++ --prefix=/usr --program-suffix=-6 --program-prefix=x86_64-linux-gnu- --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --libdir=/usr/lib --enable-nls --with-sysroot=/ --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --with-default-libstdcxx-abi=new --enable-gnu-unique-object --disable-vtable-verify --enable-libmpx --enable-plugin --enable-default-pie --with-system-zlib --disable-browser-plugin --enable-java-awt=gtk --enable-gtk-cairo --with-java-home=/usr/lib/jvm/java-1.5.0-gcj-6-amd64/jre --enable-java-home --with-jvm-root-dir=/usr/lib/jvm/java-1.5.0-gcj-6-amd64 --with-jvm-jar-dir=/usr/lib/jvm-exports/java-1.5.0-gcj-6-amd64 --with-arch-directory=amd64 --with-ecj-jar=/usr/share/java/eclipse-ecj.jar --enable-objc-gc --enable-multiarch --disable-werror --with-arch-32=i686 --with-abi=m64 --with-multilib-list=m32,m64,mx32 --enable-multilib --with-tune=generic --enable-checking=release --build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu
Thread model: posix
gcc version 6.2.0 20161005 (Ubuntu 6.2.0-5ubuntu12) 

The same in Debian:
gcc version 6.1.1 20160802 (Debian 6.1.1-11)

However, if I switch to clang, everything works as usual.

Any ideas? Thank you in advance for your help!

Understanding Question

Hello,

I am trying to work through your code, and I have a small understanding issue:
In SolverTypes.h, you define the class lbool. For the && operator of it, you are writing some optimized code; I guess to make it faster. My understanding is that lbool is one of three values: True (represented by 0), False (represented by 1), and Undefined (represented by 2). I would expect the result of the && operation, at least in theory, to be one of these three values. But when I run the lines

cout << toInt(l_True && l_True) << endl;
cout << toInt(l_True && l_False) << endl;
cout << toInt(l_True && l_Undef) << endl;
cout << toInt(l_False && l_True) << endl;
cout << toInt(l_False && l_False) << endl;
cout << toInt(l_False && l_Undef) << endl;
cout << toInt(l_Undef && l_True) << endl;
cout << toInt(l_Undef && l_False) << endl;
cout << toInt(l_Undef && l_Undef) << endl;

I get as output

0
1
3
1
1
1
3
1
3

Is that intended? Is anything that is not 0 or 1 automatically undef? This is just for my understanding. Thanks in advance for the answer.

The way Minisat actually solves CNF clauses

I have two .cnf files containing CNF clauses. Both these files solve one problem, which means that the CNF clauses in the two files are the same, but the order of CNF clauses in each file is different. I've set timeout = 1800s, but only one .cnf file can solve that problem in 1800s, the other doesn't. Hence, I wonder if the order of CNF clauses in .cnf file affects the way Minisat solve the problem or not.

unexpected results running minisat on SATLIB benchmark tests

Hi, I'm trying to benchmark another sat solver and I've tried to compare it to minisat

I'm using the benchmark set https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/uf20-91.tar.gz from

https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

they say that they're all satisfiable. I've compiled the master branch of minisat. At first it gives

PARSE ERROR! Unexpected char: %

then if I remove that last row with the % character and i run with

time for file in $(ls ~/Desktop/3SAT/uf20-91/); do cat ~/Desktop/3SAT/uf20-91/$file | grep -v '%' | build/release/bin/minisat -pre /dev/stdin /dev/stdout; done

I get all UNSATIFIABLE results like this:

WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:            20                                         |
|  Number of clauses:              91                                         |
|  Parse time:                   0.00 s                                       |
|  Simplification time:          0.00 s                                       |
|                                                                             |
UNSAT
===============================================================================
Solved by simplification
restarts              : 0
conflicts             : 0              (0 /sec)
decisions             : 0              (-nan % random) (0 /sec)
propagations          : 0              (0 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 5.94 MB
CPU time              : 0.000964 s

UNSATISFIABLE

whereas they should be all satifiable. I should be doing something wrong.

Minor logic errors in simplification

This was reported a long time ago, but no action has been taken since then. To make it conspicuous, and as a record, I am opening an issue.

Details can be found here:
https://groups.google.com/forum/#!searchin/minisat/chanseok/minisat/ldiQ82kdLzA/2NzpebK7qEkJ

Fix compilation error on non-Linux systems

The most recent commit (37dc6c6) breaks builds on non-Linux systems (or on Linux builds using Emscripten, which is how I hit it). Specifically, it adds a parameter to the Minisat::memUsedPeak function in utils/System.h but only modifies one version in utils/System.cc (under #if defined(linux)). The other copies of the function do not have the extra parameter and so no not compile.

The easiest fix is to simply modify the other three versions of this function to have the extra parameter, which they then ignore. A smarter implementation would of course use the parameter.

Read-only file system

@niklasso @koengit
I am using Mac OS Catalina to install minisat.
When I run the command " make install", I get the following errors:
install -d /include/minisat install: mkdir /include: Read-only file system make: *** [install-headers] Error 71

I has already tried for many times, but I failed.

Find a solution that contains as few values assigned to be true as possible.

Hello guys,

May I ask if there is a way to assign those useless variables to be false in SAT(or try to find the feasible solution that contains the least number of true variables)?
For example, in an already solved instance, if a variable x can either be true or false and the solution is still feasible. Then I would rather it be false, which is beneficial in my current use case,

Lastly, thanks for sharing such an elegant SAT solver!

--version

Declaration of mkLit breaks compilation on OS X (with clang-503.0.40)

When building minisat on OS X, with clang-503.0.40, the compilation breaks with the following error:

Compiling: build/release/minisat/simp/Main.o
In file included from minisat/simp/Main.cc:27:
In file included from ./minisat/core/Dimacs.h:27:
./minisat/core/SolverTypes.h:55:16: error: friend declaration specifying a default argument must be a definition
    friend Lit mkLit(Var var, bool sign = false);
               ^
./minisat/core/SolverTypes.h:63:14: error: friend declaration specifying a default argument must be the only declaration
inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
             ^
./minisat/core/SolverTypes.h:55:16: note: previous declaration is here
    friend Lit mkLit(Var var, bool sign = false);
               ^
In file included from minisat/simp/Main.cc:27:
./minisat/core/Dimacs.h:43:39: error: use of undeclared identifier 'mkLit'
        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
                                      ^
./minisat/core/Dimacs.h:43:53: error: use of undeclared identifier 'mkLit'
        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
                                                    ^
In file included from minisat/simp/Main.cc:28:
./minisat/simp/SimpSolver.h:117:70: error: use of undeclared identifier 'mkLit'
        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }
                                                                     ^
./minisat/simp/SimpSolver.h:117:99: error: use of undeclared identifier 'mkLit'
        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }
                                                                                                  ^
6 errors generated.
make: *** [build/release/minisat/simp/Main.o] Error 1

The issue seems to be with the friend declaration of mkLit within the structure Lit, which specifies a default value. According to ISO C++11 standard, such a declaration is illegal:

"If a friend declaration specifies a default argument expression, that declaration shall be a definition and shall be the only declaration of the function or function template in the translation unit.”

An obvious fix is to remove the declaration, as there is no real reason for mkLit to be declared as friend. The default value should instead be specified in the definition of mkLit.

Asymmetric branching skips clauses

Lets look at asymmetric branching code:

bool SimpSolver::asymmVar(Var v)
{
    assert(use_simplification);

    const vec<CRef>& cls = occurs.lookup(v);

    if (value(v) != l_Undef || cls.size() == 0)
        return true;

    for (int i = 0; i < cls.size(); i++)
        if (!asymm(v, cls[i]))
            return false;

    return backwardSubsumptionCheck();
}

Note that it calls asymm, wich in turn may call strengthenClause. strengthenClause removes clause from occurs, so in code above clause being at cls[i + 1] ends up at cls[i] and we skip it.
It can be tested by taking a copy of occurs.lookup(v) instead of reference --- there is a good chance of changing solver's output for almost any relatively complex sat problem (don't forget to enable asymetric branching).

Compilation bug with clang 3.4

When compiling with clang 3.4 I get:

[..]minisat/minisat/core/SolverTypes.h:55:16: error: 
      friend declaration specifying a default argument must be a definition
    friend Lit mkLit(Var var, bool sign = false);

assertion is hit in SimpSolver::relocAll

Consider the following sequence of calls:

SimpSolver::eliminate calls
Solver::simplify, which calls
Solver::removeSatisfied (which eliminates many clauses, as the solver is used incrementally, and those clauses were deleted) and then
Solver::checkGarbage, which decides to relocate memory and calls (virtually)
SimpSolver::garbageCollect which calls
SimpSolver::relocAll

Now, the following assertion in SimpSolver::relocAll is hit:

assert(subsumption_queue.size() == 0);

(because some clauses were incrementally added, and
SimpSolver::addClause_ inserts things into subsumption_queue).

Note that this scenario might be difficult to reproduce, as Solver::checkGarbage rarely calls garbageCollect, and when it does, it's usually deep in the search rather than optimisation.

--soname linker error

Hello Niklas.

I am an undergraduate student at Tokyo Institute of Technology. I have been trying to run the code for a week now. I have fixed most of the compilation errors.
But there is one error which I am not able to fix.

Every time I try to run the make install command, I keep getting a linker error.
Kindly address this issue.

Running minisat on visual studio (windows)

Hello,

I wanted some help in implementing minisat. I downloaded the required folders and when I access minisat using visual studio command prompt on windows, i am not sure what I am supposed to do to solve a SAT instance. I have an instance of size 30k clauses and 10k variables.

Please help

All lines must be postfixed with "0"

(As mentioned in the mailing list [0])

If this is true, this needs to be mentioned somewhere.
I'll type it again: All lines must end in "0".
"0" is not a variable.

Google's number one hit on how to deal with minisat [1] does not mention that circumstance. Neither does the readme. Could you please add a hint somewhere? It took me about 3 hours to find out about this. ;_;

[0] https://groups.google.com/group/minisat/msg/e759ddeeb89e65d7
[1] http://www.dwheeler.com/essays/minisat-user-guide.html

OSX Portability issues

  Hi, this patch resolves some build issues on OSX 10.9 (earlier versions are probably affected, too).

   - Apple's gcc and clang cannot build '-static' binaries (crt0.o missing).
   - The '-soname' option is '-dylib_install_name' on OSX.
   - For linking, the order of options matters.
   - minisat::memUsedPeak() definition was not matching the declaration.
   - unused arguments need to be (void) casted to avoid a compiler warning.

 Sincerely,
 H.

diff --git a/Makefile b/Makefile
index ceb9d77..7782c85 100644
--- a/Makefile
+++ b/Makefile
@@ -62,6 +62,14 @@ SORELEASE?=.0#   Declare empty to leave out from library file name.
 MINISAT_CXXFLAGS = -I. -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -Wall -Wno-parentheses -Wextra
 MINISAT_LDFLAGS  = -Wall -lz

+ifeq (Darwin,$(findstring Darwin,$(shell uname)))
+   SHARED_LDFLAGS += -shared -Wl,-dylib_install_name,$(MINISAT_DLIB).$(SOMAJOR)
+   RELEASE_LDFLAGS +=
+else
+   SHARED_LDFLAGS += -shared -Wl,-soname,$(MINISAT_DLIB).$(SOMAJOR)
+   RELEASE_LDFLAGS += -static
+endif
+
 ECHO=@echo
 ifeq ($(VERB),)
 VERB=@
@@ -96,9 +104,9 @@ $(BUILD_DIR)/dynamic/%.o:            MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC)

 ## Build-type Link-flags:
 $(BUILD_DIR)/profile/bin/$(MINISAT):       MINISAT_LDFLAGS += -pg
-$(BUILD_DIR)/release/bin/$(MINISAT):       MINISAT_LDFLAGS += --static $(MINISAT_RELSYM)
+$(BUILD_DIR)/release/bin/$(MINISAT):       MINISAT_LDFLAGS += $(RELEASE_LDFLAGS) $(MINISAT_RELSYM)
 $(BUILD_DIR)/profile/bin/$(MINISAT_CORE):  MINISAT_LDFLAGS += -pg
-$(BUILD_DIR)/release/bin/$(MINISAT_CORE):  MINISAT_LDFLAGS += --static $(MINISAT_RELSYM)
+$(BUILD_DIR)/release/bin/$(MINISAT_CORE):  MINISAT_LDFLAGS += $(RELEASE_LDFLAGS) $(MINISAT_RELSYM)

 ## Executable dependencies
 $(BUILD_DIR)/release/bin/$(MINISAT):       $(BUILD_DIR)/release/minisat/simp/Main.o $(BUILD_DIR)/release/lib/$(MINISAT_SLIB)
@@ -162,7 +170,7 @@ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB):
    $(ECHO) Linking Shared Library: $@
    $(VERB) mkdir -p $(dir $@)
-   $(VERB) $(CXX) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@ -shared -Wl,-soname,$(MINISAT_DLIB).$(SOMAJOR) $^
+   $(VERB) $(CXX) $^ $(SHARED_LDFLAGS) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@
    $(VERB) ln -sf $(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)
    $(VERB) ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)

diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc
index 21aa4ff..b353bec 100644
--- a/minisat/utils/System.cc
+++ b/minisat/utils/System.cc
@@ -77,7 +77,7 @@ double Minisat::memUsed() {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_maxrss / 1024; }
-double Minisat::memUsedPeak() { return memUsed(); }
+double Minisat::memUsedPeak(bool strictlyPeak) { (void) strictlyPeak; return memUsed(); }


 #elif defined(__APPLE__)
@@ -87,11 +87,11 @@ double Minisat::memUsed() {
     malloc_statistics_t t;
     malloc_zone_statistics(NULL, &t);
     return (double)t.max_size_in_use / (1024*1024); }
-double Minisat::memUsedPeak() { return memUsed(); }
+double Minisat::memUsedPeak(bool strictlyPeak) { (void) strictlyPeak; return memUsed(); }

 #else
 double Minisat::memUsed()     { return 0; }
-double Minisat::memUsedPeak() { return 0; }
+double Minisat::memUsedPeak(bool strictlyPeak) { (void) strictlyPeak; return 0; }
 #endif

Function 'memUsedPeak()' is not defined on all architectures.

Define it for the different architectures with either a real or "dummy" solution.

Bug caught by SWDiA5BY authors?

Hey,

I see this diff in their code relative to MiniSat:

-           if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last())) {
+           if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) {

Is this something meaningful? I am completely out-of-track of MiniSat but I thought this might be a bug they caught?

error: friend declaration of 'Minisat::Lit mkLit(Minisat::Var, bool)' specifies default arguments and isn't a definition

Compilation error with GCC13
./minisat/core/SolverTypes.h:55:16: error: friend declaration of 'Minisat::Lit mkLit(Minisat::Var, bool)' specifies default arguments and isn't a definition [-fpermissive]
55 | friend Lit mkLit(Var var, bool sign = false);
| ^~~~~
./minisat/core/SolverTypes.h:63:14: error: friend declaration of 'Minisat::Lit Minisat::mkLit(Var, bool)' specifies default arguments and isn't the only declaration [-fpermissive]
63 | inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
| ^~~~~
./minisat/core/SolverTypes.h:55:16: note: previous declaration of 'Minisat::Lit Minisat::mkLit(Var, bool)'
55 | friend Lit mkLit(Var var, bool sign = false);
| ^~~~~
In file included from ./minisat/mtl/Alg.h:24,

analyzeFinal's returned clause is not minimal

If the 2nd assumed literal has been set to the opposite value at zero level, the conflict returned should only contain that literal. However, it may contain the other (1st) literal assumed, too. As an extreme example, if there are 100 other literals assumed, and the one set at 0 decision level is the 101th, the returned conflict may contain 101 literals.

Windows binary

I have created a repository to produce a statically linked Minisat binary for Windows: minisat-for-Windows
You can download the binaries from the Releases page

Reserved user defined literal: Space needed between string and PRIi64 token

Hi,

Applications using Minisat will not compile in strict mode with latest compilers (reported with workaround for example in the README of the Open-Source synthesis tool YOSYS, https://github.com/cliffordwolf/yosys/blob/master/README#L283). This is fixed by adding a whitespace between the format string and the PRIi64 token: "%4" PRIi64.

Sincerely,
H.

/include/minisat/utils/Options.h:285:33: error: invalid suffix on literal; C++11
      requires a space between literal and identifier [-Wreserved-user-defined-literal]
            fprintf(stderr, "%4"PRIi64, range.begin);
                                ^

Correct the compiler warnings

With g++ 7.2.0 we have compiler warnings such as
/home/mathieu/GITall/GIT/Satisfiability/minisat/minisat/utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix] fprintf(stderr, "%4"PRIi64, range.begin);

Could this be addressed?

Async interrupt should not work

The Solver::interrupt(){ asynch_interrupt = true; } with bool asynch_interrupt; should not really work -- it's not clear that asynch_interrupt can be changed from another thread and the compiler is completely at liberty to optimize out the check (as I suspect it does). It should have lock/atomic/etc. primitives around it so the compiler is aware that it can be changed from elsewhere. Also note that using volatile does not fix this issue -- it does not signal the system that another thread might change the value and so it does not force a memory sync between the threads. A memory barrier is needed before every access to it from any thread, i.e. one after the change in interrupt() and one everywhere where the value of asynch_interrupt is checked.

what is cnf-file?

Can you help explain the last line in the example, how to write a cnf-file and how to use it? please!