diff --git a/.gitignore b/.gitignore index 060a130..93b6d51 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,3 @@ -/cmsat-2.9.9.tar.gz /cryptominisat-2.9.10.zip /2.9.11.tar.gz +/5.0.1.tar.gz diff --git a/cryptominisat.spec b/cryptominisat.spec index 639cdb7..32d1adf 100644 --- a/cryptominisat.spec +++ b/cryptominisat.spec @@ -1,37 +1,44 @@ Name: cryptominisat -Version: 2.9.11 -Release: 6%{?dist} +Version: 5.0.1 +Release: 1%{?dist} Summary: SAT solver -# The Mersenne Twister implementation is BSD-licensed. -# All other files are MIT-licensed. -License: MIT -URL: http://www.msoos.org/cryptominisat2/ +# Most of the code is MIT, but a few files are LGPLv2, which subsumes MIT +License: LGPLv2 +URL: http://www.msoos.org/ Source0: https://github.com/msoos/%{name}/archive/%{version}.tar.gz +# Text is from the sources, therefore under the same copyright and license as +# the code. Man page formatting contributed by Jerry James. +Source1: cryptominisat5.1 +BuildRequires: boost-devel +BuildRequires: chrpath +BuildRequires: cmake BuildRequires: gcc-c++ -BuildRequires: libtool -BuildRequires: mariadb-connector-c-devel -BuildRequires: perl-interpreter +BuildRequires: gperftools-devel +BuildRequires: m4ri-devel +BuildRequires: python2-devel +BuildRequires: swig +BuildRequires: tbb-devel +BuildRequires: vim-common BuildRequires: zlib-devel + Requires: %{name}-libs%{?_isa} = %{version}-%{release} %description -CryptoMiniSat is a SAT solver that aims to become a premiere SAT solver -with all the features and speed of successful SAT solvers, such as -MiniSat and PrecoSat. The long-term goals of CryptoMiniSat are to be an -efficient sequential, parallel and distributed solver. There are -solvers that are good at one or the other, e.g. ManySat (parallel) or -PSolver (distributed), but we wish to excel at all. - -CryptoMiniSat 2.5 won the SAT Race 2010 among 20 solvers submitted by -researchers and industry. +CryptoMiniSat is a modern, multi-threaded, feature-rich, simplifying SAT +solver. Highlights: +- Instance simplification at every point of the search (inprocessing) +- Over 100 configurable parameters to tune to specific needs +- Collection of statistical data to MySQL database + javascript-based + visualization of it +- Clean C++ and python interfaces %package devel Summary: Header files for developing with %{name} Requires: %{name}-libs%{?_isa} = %{version}-%{release} -Requires: mariadb-connector-c-devel%{?_isa} -Requires: zlib-devel%{?_isa} +Requires: m4ri-devel%{?_isa} +Requires: tbb-devel%{?_isa} %description devel Header files for developing applications that use %{name}. @@ -42,54 +49,88 @@ Summary: Cryptominisat library %description libs The %{name} library. +%package -n python2-%{name} +Summary: Python 2 interface to %{name} +Requires: %{name}-libs%{?_isa} = %{version}-%{release} + +%{?python_provide:%python_provide python-%{name}} + +%description -n python2-%{name} +Python 2 interface to %{name}. + %prep %setup -q -# Fix version number and output directory in library documentation -sed -e 's/2\.6\.0/%{version}/' \ - -e 's,/home/soos.*cryptominisat,'$PWD, \ - -i Doxyfile +# Don't override our compiler flags +sed -i 's/-O3 -mtune=native/-DNDEBUG/' CMakeLists.txt +if [ "%{_libdir}" = "%{_prefix}/lib64" ]; then + sed -i 's,${dir}/lib,&64,g' cmake/FindPkgMacros.cmake +fi -# Generate the configure script -autoreconf -fi +# Fix the python install +sed -ri 's|install |&--root %{buildroot} |' python/CMakeLists.txt %build -export CPPFLAGS="-DHAVE_MYSQL -DCMSAT_HAVE_MYSQL" -export LDFLAGS="-L%{_libdir}/mariadb" -export LIBS="-lmysqlclient" -%configure --disable-static - -# Eliminate hardcoded rpaths -sed -e 's|^hardcode_libdir_flag_spec=.*|hardcode_libdir_flag_spec=""|g' \ - -e 's|^runpath_var=LD_RUN_PATH|runpath_var=DIE_RPATH_DIE|g' \ - -i libtool - -make %{?_smp_mflags} +%cmake +%make_build %install -make install DESTDIR=%{buildroot} +%make_install -# We don't want the libtool files -rm -f %{buildroot}%{_libdir}/*.la +# Install the man page +mkdir -p %{buildroot}%{_mandir}/man1 +sed 's/@VERSION@/%{version}/' %{SOURCE1} > \ + %{buildroot}%{_mandir}/man1/cryptominisat5.1 +touch -r %{SOURCE1} %{buildroot}%{_mandir}/man1/cryptominisat5.1 + +# Move library files to where they should go +if [ "%{_libdir}" = "%{_prefix}/lib64" ]; then + mkdir -p %{buildroot}%{_libdir} + mv %{buildroot}%{_prefix}/lib/lib%{name}* %{buildroot}%{_libdir} + mv %{buildroot}%{_prefix}/lib/cmake %{buildroot}%{_libdir} + sed -i 's|%{_prefix}/lib/|%{_libdir}/|' \ + %{buildroot}%{_libdir}/cmake/cryptominisat5/*.cmake +fi + +# Remove buildroot paths from cmake files +sed -i 's|%{buildroot}||' %{buildroot}%{_libdir}/cmake/cryptominisat5/*.cmake + +# Remove rpaths +chrpath -d %{buildroot}%{_bindir}/cryptominisat5 +chrpath -d %{buildroot}%{_bindir}/cryptominisat5_simple + +# Fix permissions +chmod 0755 %{buildroot}%{python2_sitearch}/pycryptosat.so %post libs -p /sbin/ldconfig %postun libs -p /sbin/ldconfig %files -%{_bindir}/%{name} -%{_mandir}/man1/%{name}* +%doc README.markdown +%{_bindir}/cryptominisat5 +%{_bindir}/cryptominisat5_simple +%{_mandir}/man1/cryptominisat5* %files devel -%{_includedir}/cmsat/ -%{_libdir}/lib%{name}.so +%{_includedir}/cryptominisat5/ +%{_libdir}/libcryptominisat5.so +%{_libdir}/cmake/ %files libs -%doc AUTHORS NEWS README TODO -%license LICENSE-MIT -%{_libdir}/lib%{name}-%{version}.so +%doc AUTHORS +%license LICENSE-SCALMC +%{_libdir}/libcryptominisat5.so.* + +%files -n python2-%{name} +%doc python/README.rst +%license python/LICENSE +%{python2_sitearch}/pycryptosat* %changelog +* Sat Nov 25 2017 Jerry James - 5.0.1-1 +- Update to major version 5 + * Sat Sep 23 2017 Jerry James - 2.9.11-6 - Update the mariadb BR (bz 1493618) diff --git a/cryptominisat5.1 b/cryptominisat5.1 new file mode 100644 index 0000000..af0ece8 --- /dev/null +++ b/cryptominisat5.1 @@ -0,0 +1,504 @@ +.TH "CRYPTOMINISAT" "1" "@VERSION@" "Mate Soos" "User Commands" +.SH "NAME" +cryptominisat \- conflict-driven SAT solver +.SH "SYNOPSIS" +.B cryptominisat +[\fIOPTIONS\fP] <\fIinput\-files\fP> +.SH "DESCRIPTION" +.PP +CryptoMiniSat is a SAT solver, solving problems given in CNF, or conjunctive +normal form. CryptoMiniSat retains much of the API of MiniSat, but +offers more versatility and better speed on many problems. + +The program is a classical conflict-driven solver, with variable activities, +clause learning and clause deletion. It however incorporates a number of +advanced CNF simplification functionalities which should help the speed of +solving. Further, it incorporates some advanced memory-management features +that should help in getting the most out of modern CPU caches. + +The input format is that of DIMACS CNF, i.e. a header of the form + +p cnf VARS CLAUSES + +where VARS is the number of variables, and CLAUSES is the number of clauses in +the problem. It then lists the set of clauses such as: + +1 -2 0 + +which is equivalent to the 2-long clause "v1 OR NOT v2 = TRUE" + +.SH "OPTIONS" +.TP +\fB\-h,\-\-help\fP +Print help text. +.TP +\fB\-v,\-\-version\fP +Print cryptominisat's version number. +.TP +\fB\-\-input\fP = <\fIfile1\fP,\fIfile2\fP,...> +Specify the file(s) to read. +.TP +\fB\-r,\-\-random\fP = <\fIseed\fP> [0 - 2^32-1] +Sets the random seed, used for picking decision variables (default = 0). +.TP +\fB\-t,\-\-threads\fP = <\fInum\fP> [1..] +Number of threads (default is 1). +.TP +\fB\-\-sync\fP = <\fInum\fP> +Sync threads every \fInum\fP conflicts (default = 6000). +.TP +\fB\-\-maxtime\fP = <\fInum\fP> +Stop solving after this much time, print stats and exit. +.TP +\fB\-\-maxconfl\fP = <\fInum\fP> +Stop solving after this many conflicts, print stats and exit. +.TP +\fB\-\-occsimp\fP = \fI{0,1}\fP +Perform occurrence-list-based optimizations, such as variable eliminiation, +subsumption, and bounded variable addition. Default is 1. +.TP +\fB\-\-clbtwsimp\fP = <\fInum\fP> +Perform this many cleaning iterations between simplification rounds +(default = 2). +.TP +\fB\-d,\-\-drup\fP = \fI{0,1}\fP +Put DRUP verification information into this file. +.TP +\fB\-\-drupexistscheck\fP = \fI{0,1}\fP +Check if the DRUP file provided already exists (default = 1). +.TP +\fB\-\-drupdebug\fP = \fI{0,1}\fP +Output DRUP verification to the console. This is helpful to see where DRUP +fails. Use in conjunction with \fB--verb 20\fP. +.SS "RESTART" +.TP +\fB\-\-agilg\fP = <\fInum\fP> +See paper by Armin Biere on agilities. +.TP +\fB\-\-restart\fP = \fI{geom,agility,glue,glueagility}\fP +Choose the restart strategy to follow. +.TP +\fB\-\-agillim\fP = <\fInum\fP> +The agility below which the agility is considered too low (default = 0.03). +.TP +\fB\-\-agilviollim\fP = <\fInum\fP> +The number of agility violations over which to demand a restart (default = 20). +.TP +\fB\-\-gluehist\fP = <\fInum\fP> +The size of the moving window for short term glue history of redundant +clauses (default = 100). If higher, the minimal number of conflicts between +restarts is longer. +.TP +\fB\-\-blkrest\fP = \fI{0,1}\fP +Perform blocking restarts as per Glucose 3.0 (default = 1). +.TP +\fB\-\-blkrestlen\fP = <\fInum\fP> +The length of the long term trail size for blocking restart (default = 5000). +.TP +\fB\-\-blkrestmultip\fP = <\fInum\fP> +Multiplier used for blocking restart cut-off, called "R" in Glucose 3.0 +(default = 1.4). +.SS "PRINTING" +.TP +\fB\-\-verb\fP = <\fInum\fP> [0-10] +Verbosity of the solver (default = 2). Verbosity 0 only prints the results. +.TP +\fB\-\-verbstat\fP = \fI{0,1}\fP +Turns off verbose stats if needed (default = 1). +.TP +\fB\-\-printfull\fP = \fI{0,1}\fP +Print more thorough, but different, stats (default = 0). +.TP +\fB\-s,\-\-printsol\fP = \fI{0,1}\fP +Print the satisfying assignment if the solution is SAT (default = 1). +.TP +\fB\-\-printtrail\fP = <\fInum\fP> +Print the longest decision trail of the last N conflicts; if 0, the decision +trail is not printed (default = 0). +.TP +\fB\-\-printbest\fP = <\fInum\fP> +Print the best N irredundant longer-than-3 learnt clauses; if 0, nothing is +printed (default = 0). +.TP +\fB\-\-printtimes\fP = \fI{0,1}\fP +Print the time taken for each simplification run; if 0, nothing is printed, +which makes logs easier to compare (default = 1). +.SS "PROPAGATION" +.TP +\fB\-\-updateglue\fP = \fI{0,1}\fP +Update glues while propagating (default = 1). +.TP +\fB\-\-lhbr\fP = \fI{0,1}\fP +Perform lazy hyper-binary resolution while propagating (default = 0). +.TP +\fB\-\-binpri\fP = \fI{0,1}\fP +Propagated binary clauses are strictly first (default = 0). +.TP +\fB\-\-otfhyper\fP = \fI{0,1}\fP +Perform hyper-binary resolution at decision level 1 after every restart and +during probing (default = 1). +.SS "REDUNDANT CLAUSE REMOVAL" +.TP +\fB\-\-ltclean\fP = <\fInum\fP> [0-1] +Remove at least this ratio of redundant clauses when doing redundant clause +cleaning (default = 0.5). +.TP +\fB\-\-clean\fP = \fI{size,glue,activity,prconf,confdep}\fP +Metric used to clean clauses (default = prconf). Use "prconf" for the sum of +propagations and conflicts. Use "confdep" for (propagations + conflicts) / +(depth at which they were caused). +.TP +\fB\-\-noremfreshgl2\fP = \fI{0,1}\fP +Don't remove glue 2 clauses that are fresh (default = 0). +.TP +\fB\-\-cleanconflmult\fP = <\fInum\fP> +If propagations and conflicts are used to clean, the value by which conflicts +are multiplied relative to propagations (default = 1). Conflicts are much +rarer, but maybe more useful. +.TP +\fB\-\-lockuip\fP = <\fInum\fP> +The number of clauses to lock into the database per cleaning based on UIP usage +(default = 500). +.TP +\fB\-\-locktop\fP = <\fInum\fP> +The number of clauses to lock into the database per cleaning based on the best +uncleaned clauses as per the selected heuristic (default = 0). +.TP +\fB\-\-perfmult\fP = <\fInum\fP> +Value by which to multiply clause performance values after every clause cleaning +(default = 0). +.TP +\fB\-\-clearstat\fP = \fI{0,1}\fP +Clear clause statistics data of each clause after clause cleaning (default = 1). +.TP +\fB\-\-startclean\fP = <\fInum\fP> +Clean the first time after this many conflicts (default = 10000). +.TP +\fB\-\-incclean\fP = <\fInum\fP> +Clean increment cleaning by this factor for the next cleaning (default = 1.1). +.TP +\fB\-\-maxredratio\fP = <\fInum\fP> +Never have more than N * (irred_clauses) redundant clauses (default = 10). +.SS "VARIABLE BRANCHING" +.TP +\fB\-\-vincmult\fP = <\fInum\fP> +Variable activity increase multipler (default = 11). +.TP +\fB\-\-vincdiv\fP = <\fInum\fP> +Variable activity increase divider (default = 10); it \fBmust\fP be smaller +than the multiplier. +.TP +\fB\-\-vincvary\fP = <\fInum\fP> +Variable activity divider and multiplier are both changed +/- this amount, +randomly, in sync (default = 0). +.TP +\fB\-\-vincstart\fP = <\fInum\fP> +Variable activity increase stars with this value. Make sure that this, +multiplied by the multiplier and divided by the divider, is larger than itself +(default = 128). +.TP +\fB\-\-freq\fP = <\fInum\fP> [0-1] +Frequency of picking decision variables at random (default = 0). +.TP +\fB\-\-dompickf\fP = <\fInum\fP> +Use the dominating literal once in every N when picking decision literal +(default = 400). +.TP +\fB\-\-morebump\fP = \fI{0,1}\fP +Bump variables' activities based on the glue of redundant clauses there are in +during UIP generation, as per Glucose (default = 1). +.SS "VARIABLE POLARITY" +.TP +\fB\-\-polar\fP = \fI{true,false,rnd,auto}\fP +Selects the polarity mode (default = auto). True selects only positive +polarity when branching. False selects only negative polarity when branching. +Auto selects the last polarity used (also called 'caching'). +.TP +\fB\-\-calcpolar1st\fP = \fI{0,1}\fP +Calculate the polarity of variables based on their occurrences at startup of +solve() (default = 1). +.TP +\fB\-\-calcpolarall\fP = \fI{0,1}\fP +Calculate the polarity of variables based on their occurrences at startup and +after every simplification (default = 1). +.SS "CONFLICT" +.TP +\fB\-\-recur\fP = \fI{0,1}\fP +Perform recursive minimisation. +.TP +\fB\-\-moreminim\fP = \fI{0,1}\fP +Perform strong minimisation at conflict gen. +.TP +\fB\-\-moreminimcache\fP = <\fInum\fP> +Timeout in microsteps for each more minimisation with cache (default = 200). +Only active if 'moreminim' is on. +.TP +\fB\-\-moreminimbin\fP = <\fInum\fP> +Timeout in microsteps for each more minimisation with binary clauses +(default = 100). Only active if 'moreminim' is on. +.TP +\fB\-\-alwaysmoremin\fP = \fI{0,1}\fP +Always strong-minimise clauses. +.TP +\fB\-\-otfsubsume\fP = \fI{0,1}\fP +Perform on-the-fly subsumption. +.TP +\fB\-\-rewardotfsubsume\fP = <\fInum\fP> +Reward with this many propagations and conflicts a clause that has been +shortened with on-the-fly subsumption (default = 3). +.TP +\fB\-\-printimpldot\fP = \fI{0,1}\fP +Print implication graph DOT files, for input into graphviz. +.SS "ITERATIVE SOLVE" +.TP +\fB\-\-maxsol\fP = <\fInum\fP> +Search for the given number of solutions (default = 1). +.TP +\fB\-\-dumpred\fP = <\fIfilename\fP> +If stopped, dump redundant clauses here. +.TP +\fB\-\-maxdump\fP = <\fInum\fP> +Maximum length of redundant clauses to dump. +.TP +\fB\-\-dumpirred\fP = <\fIfilename\fP> +If stopped, dump irredundant original problems here. +.TP +\fB\-\-debuglib\fP +Solve at specific \fBc Solver::solve()\fP points in the CNF file. Used to +debug file generated by Solver's \fBneedLibraryCNFFile()\fP function. +.TP +\fB\-\-dumpresult\fP = <\fIfilename\fP> +Write result(s) to this file. +.SS "PROBING" +.TP +\fB\-\-bothprop\fP = \fI{0,1}\fP +Do propagations solely to propagate the same value twice (default = 1). +.TP +\fB\-\-probe\fP = \fI{0,1}\fP +Carry out probing (default = 1). +.TP +\fB\-\-probemaxm\fP = <\fInum\fP> +Time in mega-bogoprops to perform probing (default = 1900). +.TP +\fB\-\-transred\fP = \fI{0,1}\fP +Remove useless binary clauses; i.e., transitive reduction (default = 1). +.SS "STAMPING" +.TP +\fB\-\-stamp\fP = \fI{0,1}\fP +Use time stamping as per the Heule, Javisalo, and Biere paper (default = 1). +.TP +\fB\-\-cache\fP = \fI{0,1}\fP +Use an implication cache (default = 1). This option may use a lot of memory. +.TP +\fB\-\-cachesize\fP = <\fInum\fP> +Maximum size of the implication cache in MB (default = 2048). The cache may +temporarily use more memory, but will be deleted and disabled if this limit is +reached. +.TP +\fB\-\-calcreach\fP = \fI{0,1}\fP +Calculate literal reachability (default = 1). +.TP +\fB\-\-cachecutoff\fP = <\fInum\fP> +If the number of literals propagated by a literal is greater than this value, +the literal is not included in the implication cache (default = 2000). +.SS "SIMPLIFICATION" +.TP +\fB\-\-schedsimp\fP = \fI{0,1}\fP +Perform regular simplification rounds (default = 1). +.TP +\fB\-\-presimp\fP = \fI{0,1}\fP +Perform simplification at the very start (default = 0). +.TP +\fB\-\-varelim\fP = \fI{0,1}\fP +Perform variable elimination as per Een and Biere (default = 1). +.TP +\fB\-\-emptyelim\fP = \fI{0,1}\fP +Perform empty resolvent elimination using the bit-map trick (default = 1). +.TP +\fB\-\-elimstrgy\fP = \fI{heuristic,calculate}\fP +The strategy used to sort variable elimination order (default = heuristic). +The heuristic strategy uses intelligent guessing. The calculate strategy uses +exact calculation. +.TP +\fB\-\-elimcplxupd\fP = \fI{0,1}\fP +Update estimated elimination complexity on-the-fly while eliminating +(default = 1). +.TP +\fB\-\-elimcoststrategy\fP = <\fInum\fP> [0-1] +How the simple guessing strategy is calculated. +.TP +\fB\-\-strengthen\fP = \fI{0,1}\fP +Perform clause contraction through resolution (default = 1). +.TP +\fB\-\-bva\fP = \fI{0,1}\fP +Perform bounded variable addition (default = 1). +.TP +\fB\-\-bvalim\fP = <\fInum\fP> +Maximum number of variables to add by bounded variable addition per call +(default = 150000). +.TP +\fB\-\-bva2lit\fP = \fI{0,1}\fP +Bounded variable addition with 2-literal difference hack, too (default = 1). +Beware, this reduces the effectiveness of 1-literal difference. +.TP +\fB\-\-noextbinsubs\fP = \fI{0,1}\fP +No extended subsumption with binary clauses (default = 1). +.TP +\fB\-\-eratio\fP = <\fInum\fP> [0-1] +Eliminate this ratio of free variables at most per variable elimination +iteration (default = 0.12). +.TP +\fB\-\-skipresol\fP = \fI{0,1}\fP +Skip BVE resolvents in case they belong to a gate (default = 0). +.TP +\fB\-\-occredmax\fP = <\fInum\fP> +Don't add any redundant clauses larger than this to the occur list +(default = 200). +.TP +\fB\-\-occirredmaxmb\fP = <\fInum\fP> +Don't allow the irredundant occur size to be more than this many MB +(default = 800). +.TP +\fB\-\-occredmaxmb\fP = <\fInum\fP> +Don't allow the redundant occur size to be more than this many MB +(default = 800). +.SS "EQUIVALENT LITERAL" +.TP +\fB\-\-scc\fP = \fI{0,1}\fP +Find equivalent literals through SCC and replace them (default = 1). +.TP +\fB\-\-extscc\fP = \fI{0,1}\fP +Perform SCC using cache (default = 1). +.TP +\fB\-\-sccperc\fP = <\fInum\fP> [0-1] +Perform SCC only if the number of new binary clauses is at least this +percentage of the number of free variables (default = 0.02). +.SS "COMPONENT" +.TP +\fB\-\-findcomp\fP = \fI{0,1}\fP +Find components, but do not treat them (default = 0). +.TP +\fB\-\-comps\fP = \fI{0,1}\fP +Perform component-finding and separate handling (default = 1). +.TP +\fB\-\-compsfrom\fP = <\fInum\fP> +Do component finding only after this many simplification rounds (default = 0). +.TP +\fB\-\-compsvar\fP = <\fInum\fP> +Only use components when the number of variables is below this limit +(default = 1000000). +.TP +\fB\-\-compslimit\fP = <\fInum\fP> +Limit how much time is spent in component finding (default = 500). +.SS "XOR-RELATED" +.TP +\fB\-\-xor\fP = \fI{0,1}\fP +Discover long XORs (default = 1). +.TP +\fB\-\-xorcache\fP = \fI{0,1}\fP +Use cache when finding XORs (default = 0). This finds a \fIlot\fP more XORs, +but takes a lot more time. +.TP +\fB\-\-echelonxor\fP = \fI{0,1}\fP +Extract data from XORs through echelonization \fIat the top level only\fP +(default = 1). +.TP +\fB\-\-maxxormat\fP = <\fInum\fP> +The maximum matrix size (i.e., number of elements) that we should try to +echelonize (default = 10000000). +.SS "GATE-RELATED" +.TP +\fB\-\-gates\fP = \fI{0,1}\fP +Find gates (default = 1). Disables all other gate-related sub-options. +.TP +\fB\-\-gorshort\fP = \fI{0,1}\fP +Shorten clauses with OR gates (default = 1). +.TP +\fB\-\-gandrem\fP = \fI{0,1}\fP +Remove clauses with AND gates (default = 1). +.TP +\fB\-\-gateeqlit\fP = \fI{0,1}\fP +Find equivalent literals using gates (default = 1). +.TP +\fB\-\-printgatedot\fP = \fI{0,1}\fP +Print gate structure regularly to the file 'gatesX.dot' (default = 0). +.SS "SQL" +.TP +\fB\-\-sql\fP = \fI{0,1,2}\fP +Write to SQL (default = 1). 0 means do not attempt to write to the database. +1 means to try to write to the database, but continue if the attempt fails. 2 +means to abort if the database cannot be written. +.TP +\fB\-\-topnvars\fP = <\fInum\fP> +At every restart, dump data about the top N variables (default = 0). If set +to 0, nothing is dumped. +.TP +\fB\-\-dumptreevar\fP = \fI{0,1}\fP +Dump variance stats of the variables' decision and trail depths (default = 0). +.TP +\fB\-\-sqluser\fP = <\fIusername\fP> +The SQL user to connect with (default = cmsat_solver). +.TP +\fB\-\-sqlpass\fP = <\fIpassword\fP> +The SQL password to connect with. +.TP +\fB\-\-sqldb\fP = <\fIdatabase\fP> +The SQL database name (default = cmsat). The default is used by the PHP +system, so it is highly recommended. +.TP +\fB\-\-sqlserver\fP = <\fIhostname\fP> +The SQL server hostname or IP address (default = localhost). +.SS "MISCELLANEOUS" +.TP +\fB\-\-vivif\fP = \fI{0,1}\fP +Regularly execute clause vivification (default = 1). +.TP +\fB\-\-viviflongmaxm\fP = <\fInum\fP> +Maximum time in mega-bogoprops to spend on vivifying long irreducible clauses +by enqueueing and propagating (default = 20). +.TP +\fB\-\-viviffastmaxm\fP = <\fInum\fP> +Maximum time in mega-bogoprops to spend on vivifying long irreducible clauses +through watches, cache and stamps (default = 400). +.TP +\fB\-\-sortwatched\fP = \fI{0,1}\fP +Sort watches according to size (default = 1). +.TP +\fB\-\-renumber\fP = \fI{0,1}\fP +Renumber variables to increase CPU cache efficiency (default = 1). +.TP +\fB\-\-savemem\fP = \fI{0,1}\fP +Save memory by deallocating variable space after renumbering (default = 1). +This only works if renumbering is active. +.TP +\fB\-\-implicitmanip\fP = \fI{0,1}\fP +Subsume and strengthen implicit clauses with each other (default = 1). +.TP +\fB\-\-implsubsto\fP = <\fInum\fP> +The timeout of implicit subsumption in mega-bogoprops (default = 1900). +.TP +\fB\-\-burst\fP = <\fInum\fP> +The number of conflicts to do in burst search (default = 300). +.TP +\fB\-\-clearinter\fP = \fI{0,1}\fP +Interrupt threads cleanly, all the time (default = 0). +.TP +\fB\-\-zero\-exit\-status\fP = \fI{0,1}\fP +Exit with status zero in case the solving has finished without an issue. +.SH "EXIT STATUS" +.PP +The output is a solution, together with some timing information. If +\-\-zero\-exit\-status has not been specified, then the exit status is as +follows: +.IP 10 +The problem is satisfiable. +.IP 15 +The problem's satisfiability was not determined. +.IP 20 +The problem is unsatisfiable. +.SH AUTHOR +Mate Soos (soos@srlabs.de) +.SH "SEE ALSO" +The DIMACS input format can be looked up here: + +http://www.satcompetition.org/2009/format-benchmarks2009.html diff --git a/sources b/sources index 935aa3b..3fcf254 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -72b0ba94b7fc4a759d664188ad198139 2.9.11.tar.gz +SHA512 (5.0.1.tar.gz) = d9dd2eee0c801bc047101b5cbf69b3f86710811056e43ae19a3dac512f63b59c6cc85432e2cf82cfe43c4538ae8844ce5d90f3e125a48c0e3d8007f80ab6d696