New upstream release. License change to MIT. Add python3 subpackage.
This commit is contained in:
parent
66c69e8387
commit
6232da0697
|
@ -1,3 +1,3 @@
|
|||
/cryptominisat-2.9.10.zip
|
||||
/2.9.11.tar.gz
|
||||
/5.0.1.tar.gz
|
||||
/cryptominisat-*.tar.gz
|
||||
|
|
|
@ -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("$<$<CONFIG:RELWITHDEBINFO>:-O2>")
|
||||
- add_compile_options("$<$<CONFIG:RELWITHDEBINFO>:-mtune=native>")
|
||||
|
||||
add_compile_options("$<$<CONFIG:RELEASE>:-O2>")
|
||||
add_compile_options("$<$<CONFIG:RELEASE>:-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")
|
|
@ -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 <loganjerry@gmail.com> - 5.6.3-1
|
||||
- New upstream release
|
||||
- License change to MIT
|
||||
- Add python3 subpackage
|
||||
|
||||
* Wed Feb 07 2018 Fedora Release Engineering <releng@fedoraproject.org> - 5.0.1-3
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
|
||||
|
||||
|
|
504
cryptominisat5.1
504
cryptominisat5.1
|
@ -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
|
2
sources
2
sources
|
@ -1 +1 @@
|
|||
SHA512 (5.0.1.tar.gz) = d9dd2eee0c801bc047101b5cbf69b3f86710811056e43ae19a3dac512f63b59c6cc85432e2cf82cfe43c4538ae8844ce5d90f3e125a48c0e3d8007f80ab6d696
|
||||
SHA512 (cryptominisat-5.6.3.tar.gz) = 65ef3cd55f06330eac2d06bde2d7b73c595637b6c33265e79c2c38cdb17819ab1c00056a78a320d4f154a941d0bf465d6109671e018b4da14549c81f97f8281f
|
||||
|
|
Loading…
Reference in New Issue