From 6232da0697e2861fd7d92cdbda11ed1942239f8c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 12 Jun 2018 20:45:10 -0600 Subject: [PATCH] New upstream release. License change to MIT. Add python3 subpackage. --- .gitignore | 2 +- cryptominisat-cmake.patch | 53 ++++ cryptominisat.spec | 87 ++++--- cryptominisat5.1 | 504 -------------------------------------- sources | 2 +- 5 files changed, 102 insertions(+), 546 deletions(-) create mode 100644 cryptominisat-cmake.patch delete mode 100644 cryptominisat5.1 diff --git a/.gitignore b/.gitignore index 93b6d51..f2c53d7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,3 @@ -/cryptominisat-2.9.10.zip /2.9.11.tar.gz /5.0.1.tar.gz +/cryptominisat-*.tar.gz diff --git a/cryptominisat-cmake.patch b/cryptominisat-cmake.patch new file mode 100644 index 0000000..3aa093f --- /dev/null +++ b/cryptominisat-cmake.patch @@ -0,0 +1,53 @@ +--- CMakeLists.txt.orig 2018-06-10 23:39:47.000000000 -0600 ++++ CMakeLists.txt 2018-06-12 14:55:02.159208716 -0600 +@@ -172,8 +172,6 @@ if (ENABLE_ASSERTIONS) + else() + # Note this definition doesn't appear in the cache variables. + add_definitions(-DNDEBUG) +- add_cxx_flag_if_supported("-fno-stack-protector") +- add_definitions(-D_FORTIFY_SOURCE=0) + endif() + + # Note: O3 gives slight speed increase, 1 more solved from SAT Comp'14 @ 3600s +@@ -182,7 +180,6 @@ if (NOT MSVC) + add_compile_options( -pthread ) + + add_compile_options("$<$:-O2>") +- add_compile_options("$<$:-mtune=native>") + + add_compile_options("$<$:-O2>") + add_compile_options("$<$:-g0>") +@@ -280,14 +277,10 @@ if (NOT WIN32) + if(CMAKE_BUILD_TYPE STREQUAL "Release") + #add_cxx_flag_if_supported("-flto") + else() +- add_cxx_flag_if_supported("-mtune=native") + add_cxx_flag_if_supported("-Wall") + add_cxx_flag_if_supported("-Wextra") + add_cxx_flag_if_supported("-Wunused") + add_cxx_flag_if_supported("-Wsign-compare") +- if (NOT CMAKE_BUILD_TYPE STREQUAL "Release") +- add_cxx_flag_if_supported("-fno-omit-frame-pointer") +- endif() + add_cxx_flag_if_supported("-Wtype-limits") + add_cxx_flag_if_supported("-Wuninitialized") + add_cxx_flag_if_supported("-Wno-deprecated") +@@ -299,7 +292,6 @@ if (NOT WIN32) + add_cxx_flag_if_supported("-Winit-self") + add_cxx_flag_if_supported("-Wparentheses") + add_cxx_flag_if_supported("-Wunreachable-code") +- add_cxx_flag_if_supported("-ggdb3") + endif() + endif() + +@@ -319,10 +311,6 @@ endif() + # ----------------------------------------------------------------------------- + # Uncomment these for static compilation under Linux (messes up Valgrind) + # ----------------------------------------------------------------------------- +-if (${CMAKE_SYSTEM_NAME} MATCHES "Linux" AND NOT SANITIZE) +- set(CMAKE_EXE_LINKER_FLAGS " ${CMAKE_EXE_LINKER_FLAGS} -Wl,--discard-all -Wl,--build-id=sha1") +-endif() +- + if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux") OR (${CMAKE_SYSTEM_NAME} MATCHES "Darwin")) + if(STATICCOMPILE) + MESSAGE(STATUS "Compiling for static library use") diff --git a/cryptominisat.spec b/cryptominisat.spec index d4c9fc8..a7a578d 100644 --- a/cryptominisat.spec +++ b/cryptominisat.spec @@ -1,26 +1,23 @@ Name: cryptominisat -Version: 5.0.1 -Release: 3%{?dist} +Version: 5.6.3 +Release: 1%{?dist} Summary: SAT solver -# Most of the code is MIT, but a few files are LGPLv2, which subsumes MIT -License: LGPLv2 +License: MIT 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 +Source0: https://github.com/msoos/%{name}/archive/%{version}/%{name}-%{version}.tar.gz +# Change the CMake files to not change Fedora build flags +Patch0: %{name}-cmake.patch BuildRequires: boost-devel -BuildRequires: chrpath BuildRequires: cmake BuildRequires: gcc-c++ BuildRequires: gperftools-devel +BuildRequires: help2man BuildRequires: m4ri-devel BuildRequires: python2-devel -BuildRequires: swig +BuildRequires: python3-devel BuildRequires: tbb-devel -BuildRequires: vim-common BuildRequires: zlib-devel Requires: %{name}-libs%{?_isa} = %{version}-%{release} @@ -53,16 +50,24 @@ The %{name} library. Summary: Python 2 interface to %{name} Requires: %{name}-libs%{?_isa} = %{version}-%{release} -%{?python_provide:%python_provide python-%{name}} +%{?python_provide:%python_provide python2-%{name}} %description -n python2-%{name} Python 2 interface to %{name}. -%prep -%setup -q +%package -n python3-%{name} +Summary: Python 3 interface to %{name} +Requires: %{name}-libs%{?_isa} = %{version}-%{release} -# Don't override our compiler flags -sed -i 's/-O3 -mtune=native/-DNDEBUG/' CMakeLists.txt +%{?python_provide:%python_provide python3-%{name}} + +%description -n python3-%{name} +Python 3 interface to %{name}. + +%prep +%autosetup -p0 + +# Fix the library install path if [ "%{_libdir}" = "%{_prefix}/lib64" ]; then sed -i 's,${dir}/lib,&64,g' cmake/FindPkgMacros.cmake fi @@ -70,41 +75,33 @@ fi # Fix the python install sed -ri 's|install |&--root %{buildroot} |' python/CMakeLists.txt +# Prepare to build for both python 2 and 3 +cp -a . ../python3 + %build -%cmake +%cmake -DCMAKE_INSTALL_LIBDIR=%{_lib} -DFORCE_PYTHON2=ON %make_build +pushd ../python3 +%cmake -DCMAKE_INSTALL_LIBDIR=%{_lib} +%make_build +popd + %install +pushd ../python3 +%make_install +popd + %make_install -# 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 +# Move cmake 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 +%ldconfig_scriptlets libs %files %doc README.markdown @@ -119,7 +116,7 @@ chmod 0755 %{buildroot}%{python2_sitearch}/pycryptosat.so %files libs %doc AUTHORS -%license LICENSE-SCALMC +%license LICENSE.txt %{_libdir}/libcryptominisat5.so.* %files -n python2-%{name} @@ -127,7 +124,17 @@ chmod 0755 %{buildroot}%{python2_sitearch}/pycryptosat.so %license python/LICENSE %{python2_sitearch}/pycryptosat* +%files -n python3-%{name} +%doc python/README.rst +%license python/LICENSE +%{python3_sitearch}/pycryptosat* + %changelog +* Tue Jun 12 2018 Jerry James - 5.6.3-1 +- New upstream release +- License change to MIT +- Add python3 subpackage + * Wed Feb 07 2018 Fedora Release Engineering - 5.0.1-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild diff --git a/cryptominisat5.1 b/cryptominisat5.1 deleted file mode 100644 index af0ece8..0000000 --- a/cryptominisat5.1 +++ /dev/null @@ -1,504 +0,0 @@ -.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 3fcf254..d6a3ba5 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (5.0.1.tar.gz) = d9dd2eee0c801bc047101b5cbf69b3f86710811056e43ae19a3dac512f63b59c6cc85432e2cf82cfe43c4538ae8844ce5d90f3e125a48c0e3d8007f80ab6d696 +SHA512 (cryptominisat-5.6.3.tar.gz) = 65ef3cd55f06330eac2d06bde2d7b73c595637b6c33265e79c2c38cdb17819ab1c00056a78a320d4f154a941d0bf465d6109671e018b4da14549c81f97f8281f