niklasso / minisat Goto Github PK
View Code? Open in Web Editor NEWA minimalistic and high-performance SAT solver
Home Page: minisat.se
License: Other
A minimalistic and high-performance SAT solver
Home Page: minisat.se
License: Other
================================================================================ Quick Install - Decide where to install the files . The simplest approach is to use GNU standard locations and just set a "prefix" for the root install directory (reffered to as $PREFIX below). More control can be achieved by overriding other of the GNU standard install locations (includedir, bindir, etc). Configuring with just a prefix: > make config prefix=$PREFIX - Compiling and installing: > make install ================================================================================ Configuration - Multiple configuration steps can be joined into one call to "make config" by appending multiple variable assignments on the same line. - The configuration is stored in the file "config.mk". Look here if you want to know what the current configuration looks like. - To reset from defaults simply remove the "config.mk" file or call "make distclean". - Recompilation can be done without the configuration step. [ TODO: describe configartion possibilities for compile flags / modes ] ================================================================================ Building [ TODO: describe seperate build modes ] ================================================================================ Install [ TODO: ? ] ================================================================================ Directory Overview: minisat/mtl/ Mini Template Library minisat/utils/ Generic helper code (I/O, Parsing, CPU-time, etc) minisat/core/ A core version of the solver minisat/simp/ An extended solver with simplification capabilities doc/ Documentation README LICENSE ================================================================================ Examples: Run minisat with same heuristics as version 2.0: > minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02
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!
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.
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.
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.
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
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.
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!
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.
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).
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);
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.
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.
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
(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
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
Define it for the different architectures with either a real or "dummy" solution.
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?
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,
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.
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
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);
^
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?
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.
Can you help explain the last line in the example, how to write a cnf-file and how to use it? please!
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.