diff options
Diffstat (limited to 'src/prop/cryptominisat/man')
| -rw-r--r-- | src/prop/cryptominisat/man/Makefile.am | 2 | ||||
| -rw-r--r-- | src/prop/cryptominisat/man/Makefile.in | 439 | ||||
| -rw-r--r-- | src/prop/cryptominisat/man/cryptominisat.1 | 228 |
3 files changed, 0 insertions, 669 deletions
diff --git a/src/prop/cryptominisat/man/Makefile.am b/src/prop/cryptominisat/man/Makefile.am deleted file mode 100644 index a28b612b3..000000000 --- a/src/prop/cryptominisat/man/Makefile.am +++ /dev/null @@ -1,2 +0,0 @@ -man_MANS = cryptominisat.1 -EXTRA_DIST = $(man_MANS) diff --git a/src/prop/cryptominisat/man/Makefile.in b/src/prop/cryptominisat/man/Makefile.in deleted file mode 100644 index 5542511eb..000000000 --- a/src/prop/cryptominisat/man/Makefile.in +++ /dev/null @@ -1,439 +0,0 @@ -# Makefile.in generated by automake 1.11.1 from Makefile.am. -# @configure_input@ - -# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002, -# 2003, 2004, 2005, 2006, 2007, 2008, 2009 Free Software Foundation, -# Inc. -# This Makefile.in is free software; the Free Software Foundation -# gives unlimited permission to copy and/or distribute it, -# with or without modifications, as long as this notice is preserved. - -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY, to the extent permitted by law; without -# even the implied warranty of MERCHANTABILITY or FITNESS FOR A -# PARTICULAR PURPOSE. - -@SET_MAKE@ -VPATH = @srcdir@ -pkgdatadir = $(datadir)/@PACKAGE@ -pkgincludedir = $(includedir)/@PACKAGE@ -pkglibdir = $(libdir)/@PACKAGE@ -pkglibexecdir = $(libexecdir)/@PACKAGE@ -am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd -install_sh_DATA = $(install_sh) -c -m 644 -install_sh_PROGRAM = $(install_sh) -c -install_sh_SCRIPT = $(install_sh) -c -INSTALL_HEADER = $(INSTALL_DATA) -transform = $(program_transform_name) -NORMAL_INSTALL = : -PRE_INSTALL = : -POST_INSTALL = : -NORMAL_UNINSTALL = : -PRE_UNINSTALL = : -POST_UNINSTALL = : -build_triplet = @build@ -host_triplet = @host@ -subdir = man -DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in -ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/configure.in -am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ - $(ACLOCAL_M4) -mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = $(top_builddir)/config.h -CONFIG_CLEAN_FILES = -CONFIG_CLEAN_VPATH_FILES = -SOURCES = -DIST_SOURCES = -am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; -am__vpath_adj = case $$p in \ - $(srcdir)/*) f=`echo "$$p" | sed "s|^$$srcdirstrip/||"`;; \ - *) f=$$p;; \ - esac; -am__strip_dir = f=`echo $$p | sed -e 's|^.*/||'`; -am__install_max = 40 -am__nobase_strip_setup = \ - srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*|]/\\\\&/g'` -am__nobase_strip = \ - for p in $$list; do echo "$$p"; done | sed -e "s|$$srcdirstrip/||" -am__nobase_list = $(am__nobase_strip_setup); \ - for p in $$list; do echo "$$p $$p"; done | \ - sed "s| $$srcdirstrip/| |;"' / .*\//!s/ .*/ ./; s,\( .*\)/[^/]*$$,\1,' | \ - $(AWK) 'BEGIN { files["."] = "" } { files[$$2] = files[$$2] " " $$1; \ - if (++n[$$2] == $(am__install_max)) \ - { print $$2, files[$$2]; n[$$2] = 0; files[$$2] = "" } } \ - END { for (dir in files) print dir, files[dir] }' -am__base_list = \ - sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \ - sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g' -man1dir = $(mandir)/man1 -am__installdirs = "$(DESTDIR)$(man1dir)" -NROFF = nroff -MANS = $(man_MANS) -DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) -ACLOCAL = @ACLOCAL@ -AMTAR = @AMTAR@ -AR = @AR@ -AUTOCONF = @AUTOCONF@ -AUTOHEADER = @AUTOHEADER@ -AUTOMAKE = @AUTOMAKE@ -AWK = @AWK@ -CC = @CC@ -CCDEPMODE = @CCDEPMODE@ -CFLAGS = @CFLAGS@ -CPP = @CPP@ -CPPFLAGS = @CPPFLAGS@ -CXX = @CXX@ -CXXCPP = @CXXCPP@ -CXXDEPMODE = @CXXDEPMODE@ -CXXFLAGS = @CXXFLAGS@ -CYGPATH_W = @CYGPATH_W@ -DEFS = @DEFS@ -DEPDIR = @DEPDIR@ -DLLTOOL = @DLLTOOL@ -DSYMUTIL = @DSYMUTIL@ -DUMPBIN = @DUMPBIN@ -ECHO_C = @ECHO_C@ -ECHO_N = @ECHO_N@ -ECHO_T = @ECHO_T@ -EGREP = @EGREP@ -EXEEXT = @EXEEXT@ -FGREP = @FGREP@ -GREP = @GREP@ -INSTALL = @INSTALL@ -INSTALL_DATA = @INSTALL_DATA@ -INSTALL_PROGRAM = @INSTALL_PROGRAM@ -INSTALL_SCRIPT = @INSTALL_SCRIPT@ -INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ -LD = @LD@ -LDFLAGS = @LDFLAGS@ -LIBOBJS = @LIBOBJS@ -LIBS = @LIBS@ -LIBTOOL = @LIBTOOL@ -LIPO = @LIPO@ -LN_S = @LN_S@ -LTLIBOBJS = @LTLIBOBJS@ -MAKEINFO = @MAKEINFO@ -MANIFEST_TOOL = @MANIFEST_TOOL@ -MKDIR_P = @MKDIR_P@ -NM = @NM@ -NMEDIT = @NMEDIT@ -OBJDUMP = @OBJDUMP@ -OBJEXT = @OBJEXT@ -OPENMP_CXXFLAGS = @OPENMP_CXXFLAGS@ -OTOOL = @OTOOL@ -OTOOL64 = @OTOOL64@ -PACKAGE = @PACKAGE@ -PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@ -PACKAGE_NAME = @PACKAGE_NAME@ -PACKAGE_STRING = @PACKAGE_STRING@ -PACKAGE_TARNAME = @PACKAGE_TARNAME@ -PACKAGE_URL = @PACKAGE_URL@ -PACKAGE_VERSION = @PACKAGE_VERSION@ -PATH_SEPARATOR = @PATH_SEPARATOR@ -RANLIB = @RANLIB@ -SED = @SED@ -SET_MAKE = @SET_MAKE@ -SHELL = @SHELL@ -STRIP = @STRIP@ -VERSION = @VERSION@ -abs_builddir = @abs_builddir@ -abs_srcdir = @abs_srcdir@ -abs_top_builddir = @abs_top_builddir@ -abs_top_srcdir = @abs_top_srcdir@ -ac_ct_AR = @ac_ct_AR@ -ac_ct_CC = @ac_ct_CC@ -ac_ct_CXX = @ac_ct_CXX@ -ac_ct_DUMPBIN = @ac_ct_DUMPBIN@ -am__include = @am__include@ -am__leading_dot = @am__leading_dot@ -am__quote = @am__quote@ -am__tar = @am__tar@ -am__untar = @am__untar@ -bindir = @bindir@ -build = @build@ -build_alias = @build_alias@ -build_cpu = @build_cpu@ -build_os = @build_os@ -build_vendor = @build_vendor@ -builddir = @builddir@ -datadir = @datadir@ -datarootdir = @datarootdir@ -docdir = @docdir@ -dvidir = @dvidir@ -exec_prefix = @exec_prefix@ -host = @host@ -host_alias = @host_alias@ -host_cpu = @host_cpu@ -host_os = @host_os@ -host_vendor = @host_vendor@ -htmldir = @htmldir@ -includedir = @includedir@ -infodir = @infodir@ -install_sh = @install_sh@ -libdir = @libdir@ -libexecdir = @libexecdir@ -localedir = @localedir@ -localstatedir = @localstatedir@ -mandir = @mandir@ -mkdir_p = @mkdir_p@ -oldincludedir = @oldincludedir@ -pdfdir = @pdfdir@ -prefix = @prefix@ -program_transform_name = @program_transform_name@ -psdir = @psdir@ -sbindir = @sbindir@ -sharedstatedir = @sharedstatedir@ -srcdir = @srcdir@ -sysconfdir = @sysconfdir@ -target_alias = @target_alias@ -top_build_prefix = @top_build_prefix@ -top_builddir = @top_builddir@ -top_srcdir = @top_srcdir@ -man_MANS = cryptominisat.1 -EXTRA_DIST = $(man_MANS) -all: all-am - -.SUFFIXES: -$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) - @for dep in $?; do \ - case '$(am__configure_deps)' in \ - *$$dep*) \ - ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \ - && { if test -f $@; then exit 0; else break; fi; }; \ - exit 1;; \ - esac; \ - done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu man/Makefile'; \ - $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --gnu man/Makefile -.PRECIOUS: Makefile -Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status - @case '$?' in \ - *config.status*) \ - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \ - *) \ - echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \ - cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \ - esac; - -$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh - -$(top_srcdir)/configure: $(am__configure_deps) - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(ACLOCAL_M4): $(am__aclocal_m4_deps) - cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(am__aclocal_m4_deps): - -mostlyclean-libtool: - -rm -f *.lo - -clean-libtool: - -rm -rf .libs _libs -install-man1: $(man_MANS) - @$(NORMAL_INSTALL) - test -z "$(man1dir)" || $(MKDIR_P) "$(DESTDIR)$(man1dir)" - @list=''; test -n "$(man1dir)" || exit 0; \ - { for i in $$list; do echo "$$i"; done; \ - l2='$(man_MANS)'; for i in $$l2; do echo "$$i"; done | \ - sed -n '/\.1[a-z]*$$/p'; \ - } | while read p; do \ - if test -f $$p; then d=; else d="$(srcdir)/"; fi; \ - echo "$$d$$p"; echo "$$p"; \ - done | \ - sed -e 'n;s,.*/,,;p;h;s,.*\.,,;s,^[^1][0-9a-z]*$$,1,;x' \ - -e 's,\.[0-9a-z]*$$,,;$(transform);G;s,\n,.,' | \ - sed 'N;N;s,\n, ,g' | { \ - list=; while read file base inst; do \ - if test "$$base" = "$$inst"; then list="$$list $$file"; else \ - echo " $(INSTALL_DATA) '$$file' '$(DESTDIR)$(man1dir)/$$inst'"; \ - $(INSTALL_DATA) "$$file" "$(DESTDIR)$(man1dir)/$$inst" || exit $$?; \ - fi; \ - done; \ - for i in $$list; do echo "$$i"; done | $(am__base_list) | \ - while read files; do \ - test -z "$$files" || { \ - echo " $(INSTALL_DATA) $$files '$(DESTDIR)$(man1dir)'"; \ - $(INSTALL_DATA) $$files "$(DESTDIR)$(man1dir)" || exit $$?; }; \ - done; } - -uninstall-man1: - @$(NORMAL_UNINSTALL) - @list=''; test -n "$(man1dir)" || exit 0; \ - files=`{ for i in $$list; do echo "$$i"; done; \ - l2='$(man_MANS)'; for i in $$l2; do echo "$$i"; done | \ - sed -n '/\.1[a-z]*$$/p'; \ - } | sed -e 's,.*/,,;h;s,.*\.,,;s,^[^1][0-9a-z]*$$,1,;x' \ - -e 's,\.[0-9a-z]*$$,,;$(transform);G;s,\n,.,'`; \ - test -z "$$files" || { \ - echo " ( cd '$(DESTDIR)$(man1dir)' && rm -f" $$files ")"; \ - cd "$(DESTDIR)$(man1dir)" && rm -f $$files; } -tags: TAGS -TAGS: - -ctags: CTAGS -CTAGS: - - -distdir: $(DISTFILES) - @list='$(MANS)'; if test -n "$$list"; then \ - list=`for p in $$list; do \ - if test -f $$p; then d=; else d="$(srcdir)/"; fi; \ - if test -f "$$d$$p"; then echo "$$d$$p"; else :; fi; done`; \ - if test -n "$$list" && \ - grep 'ab help2man is required to generate this page' $$list >/dev/null; then \ - echo "error: found man pages containing the \`missing help2man' replacement text:" >&2; \ - grep -l 'ab help2man is required to generate this page' $$list | sed 's/^/ /' >&2; \ - echo " to fix them, install help2man, remove and regenerate the man pages;" >&2; \ - echo " typically \`make maintainer-clean' will remove them" >&2; \ - exit 1; \ - else :; fi; \ - else :; fi - @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ - topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ - list='$(DISTFILES)'; \ - dist_files=`for file in $$list; do echo $$file; done | \ - sed -e "s|^$$srcdirstrip/||;t" \ - -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \ - case $$dist_files in \ - */*) $(MKDIR_P) `echo "$$dist_files" | \ - sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \ - sort -u` ;; \ - esac; \ - for file in $$dist_files; do \ - if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \ - if test -d $$d/$$file; then \ - dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \ - if test -d "$(distdir)/$$file"; then \ - find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ - fi; \ - if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \ - cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \ - find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \ - fi; \ - cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \ - else \ - test -f "$(distdir)/$$file" \ - || cp -p $$d/$$file "$(distdir)/$$file" \ - || exit 1; \ - fi; \ - done -check-am: all-am -check: check-am -all-am: Makefile $(MANS) -installdirs: - for dir in "$(DESTDIR)$(man1dir)"; do \ - test -z "$$dir" || $(MKDIR_P) "$$dir"; \ - done -install: install-am -install-exec: install-exec-am -install-data: install-data-am -uninstall: uninstall-am - -install-am: all-am - @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am - -installcheck: installcheck-am -install-strip: - $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ - install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ - `test -z '$(STRIP)' || \ - echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install -mostlyclean-generic: - -clean-generic: - -distclean-generic: - -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES) - -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES) - -maintainer-clean-generic: - @echo "This command is intended for maintainers to use" - @echo "it deletes files that may require special tools to rebuild." -clean: clean-am - -clean-am: clean-generic clean-libtool mostlyclean-am - -distclean: distclean-am - -rm -f Makefile -distclean-am: clean-am distclean-generic - -dvi: dvi-am - -dvi-am: - -html: html-am - -html-am: - -info: info-am - -info-am: - -install-data-am: install-man - -install-dvi: install-dvi-am - -install-dvi-am: - -install-exec-am: - -install-html: install-html-am - -install-html-am: - -install-info: install-info-am - -install-info-am: - -install-man: install-man1 - -install-pdf: install-pdf-am - -install-pdf-am: - -install-ps: install-ps-am - -install-ps-am: - -installcheck-am: - -maintainer-clean: maintainer-clean-am - -rm -f Makefile -maintainer-clean-am: distclean-am maintainer-clean-generic - -mostlyclean: mostlyclean-am - -mostlyclean-am: mostlyclean-generic mostlyclean-libtool - -pdf: pdf-am - -pdf-am: - -ps: ps-am - -ps-am: - -uninstall-am: uninstall-man - -uninstall-man: uninstall-man1 - -.MAKE: install-am install-strip - -.PHONY: all all-am check check-am clean clean-generic clean-libtool \ - distclean distclean-generic distclean-libtool distdir dvi \ - dvi-am html html-am info info-am install install-am \ - install-data install-data-am install-dvi install-dvi-am \ - install-exec install-exec-am install-html install-html-am \ - install-info install-info-am install-man install-man1 \ - install-pdf install-pdf-am install-ps install-ps-am \ - install-strip installcheck installcheck-am installdirs \ - maintainer-clean maintainer-clean-generic mostlyclean \ - mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \ - uninstall uninstall-am uninstall-man uninstall-man1 - - -# Tell versions [3.59,3.63) of GNU make to not export all variables. -# Otherwise a system limit (for SysV at least) may be exceeded. -.NOEXPORT: diff --git a/src/prop/cryptominisat/man/cryptominisat.1 b/src/prop/cryptominisat/man/cryptominisat.1 deleted file mode 100644 index 2fffa82e8..000000000 --- a/src/prop/cryptominisat/man/cryptominisat.1 +++ /dev/null @@ -1,228 +0,0 @@ -.TH "CRYPTOMINISAT" "1" "@VERSION@" "Mate Soos" "User Commands" -.SH "NAME" -cryptominisat \- conflict-driven SAT solver -.SH "SYNOPSIS" -.B cryptominisat -[\fIOPTIONS\fP] <\fIinput\-file\fP> <\fIoutput\-file\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\-\-polarity\-mode\fP = \fI{true,false,rnd,auto}\fP [default: auto] -Selects the polarity mode. Auto is the Jeroslow&Wang method. -.TP -\fB\-\-rnd\-freq\fP = <\fInum\fP> [0-1] How often should decision variables -be picked randomly. -.TP -\fB\-\-verbosity\fP = <\fInum\fP> [0-2] Verbosity 1 is default. Verbosity 0 -only prints the results, and verbosity 2 prints many useful debug info. -.TP -\fB\-\-randomize\fP = <\fIseed\fP> [0 - 2^32-1] -Sets the random seed, used for picking decision variables (default = 0). -.TP -\fB\-\-restrict\fP = <\fInum\fP> [1 - varnum] -When picking random variables to branch on, pick one that is in the \fInum\fP -most active vars useful for cryptographic problems, where the question is the -key, which is usually small (e.g., 80 bits). -.TP -\fB\-\-gaussuntil\fP = <\fInum\fP> -Depth until which Gaussian elimination is active. Giving 0 switches off -Gaussian elimination. -.TP -\fB\-\-restarts\fP = <\fInum\fP> [1 - 2^32-1] -No more than the given number of restarts will be performed during search. -.TP -\fB\-\-nonormxorfind\fP -Don't find and collect >2-long xor-clauses from regular clauses. -.TP -\fB\-\-nobinxorfind\fP -Don't find and collect 2-long xor-clauses from regular clauses. -.TP -\fB\-\-noregbxorfind\fP -Don't regularly find and collect 2-long xor-clauses from regular clauses. -.TP -\fB\-\-doextendedscc\fP -Do strongly connected component finding using non-existent binary clauses. -Makes binary XOR findig slower, but somewhat more accurate. -.TP -\fB\-\-noconglomerate\fP -Don't conglomerate 2 xor clauses when one var is dependent. This allows for -elimination of variable y if it is only in the two XOR clauses "y XOR a XOR b" and -"y XOR c XOR d" -.TP -\fB\-\-nosimplify\fP -Don't do regular simplification rounds. These simplification rounds greatly -simplify the CNF, but cost time. If your problem is very small, it may be -only a waste of time to execute these simplification rounds. Typically, however, -these simplification methods save significant amount of time (>60%) -.TP -\fB\-\-greedyunbound\fP -Greedily unbound variables that are not needed for the final satisfying -assignement. -.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\-\-debugnewvar\fP -Add new vars at specific \fBc Solver::newVar()\fP points in the CNF file. -Used to debug file generated by Solver's \fBneedLibraryCNFFile()\fP function. -.TP -\fB\-\-novarreplace\fP -Don't perform variable replacement. Needed for programmable solver feature. -.TP -\fB\-\-restart\fP = \fI{auto, static, dynamic}\fP -Which kind of restart strategy to follow. Default is \fIauto\fP. -.TP -\fB\-\-dumplearnts\fP = <\fIfilename\fP> -If interrupted or reached restart limit, dump the learnt clauses to the -specified file. Maximum size of dumped clauses can be specified with the -\fB\-\-maxdumplearnts\fP option. -.TP -\fB\-\-maxdumplearnts\fP = [0 - 2^32-1] -When dumping the learnts to file, what should be maximum length of the clause -dumped. Useful to make the resulting file smaller. Default is 2^32-1. Note: -2-long XORs are always dumped. -.TP -\fB\-\-dumporig\fP = <\fIfilename\fP> -If interrupted or reached restart limit, dump the original problem instance, -simplified to the current point. -.TP -\fB\-\-alsoread\fP = <\fIfilename\fP> -Also read this file in. Can be used to re-read dumped learnts, for example. -.TP -\fB\-\-maxsolutions\fP = <\fInum\fP> -Search for given amount of solutions. Can only be used in single-threaded -mode (\fB--threads=1\fP). -.TP -\fB\-\-pavgbranch\fP -Print average branch depth. -.TP -\fB\-\-nofailedlit\fP -Don't search for failed literals, and don't search for literals propagated -both by \fIvarX\fP and \fI-varX\fP. -.TP -\fB\-\-noheuleprocess\fP -Don't try to minimise XORs by XOR-ing them together. Algorithm as per -global/local substitution in Heule's thesis. -.TP -\fB\-\-nosatelite\fP -Don't do clause subsumption, clause strengthening and variable elimination -(implies \fB\-\-novarelim\fP and \fB\-\-nosubsume1\fP). -.TP -\fB\-\-noxorsubs\fP -Don't try to subsume xor-clauses. -.TP -\fB\-\-nosolprint\fP -Don't print the satisfying assignment if the solution is SAT. -.TP -\fB\-\-novarelim\fP -Don't perform variable elimination as per Een and Biere. -.TP -\fB\-\-nosubsume1\fP -Don't perform clause contraction through resolution. -.TP -\fB\-\-noparthandler\fP -Don't find and solve subroblems with subsolvers. -.TP -\fB\-\-nomatrixfind\fP -Don't find distinct matrixes. Put all xors into one big matrix. -.TP -\fB\-\-noordercol\fP -Don't order variables in the columns of Gaussian elimination. Effectively -disables iterative reduction of the matrix. -.TP -\fB\-\-noiterreduce\fP -Don't reduce iteratively the matrix that is updated. -.TP -\fB\-\-maxmatrixrows\fP = [0 - 2^32-1] -Set maximum number of rows for gaussian matrix. Too large matrixes should be -discarded for reasons of efficiency. Default: 1000. -.TP -\fB\-\-minmatrixrows\fP = [0 - 2^32-1] -Set minimum number of rows for gaussian matrix. Normally, too small matrixes -are discarded for reasons of efficiency. Default: 20. -.TP -\fB\-\-savematrix\fP = [0 - 2^32-1] -Save matrix every Nth decision level. Default: 2. -.TP -\fB\-\-maxnummatrixes\fP = [0 - 2^32-1] -Maximum number of matrixes to treat. Default: 3. -.TP -\fB\-\-nohyperbinres\fP -Don't add binary clauses when doing failed lit probing. -.TP -\fB\-\-noremovebins\fP -Don't remove useless binary clauses. -.TP -\fB\-\-noremlbins\fP -Don't remove useless learnt binary clauses. -.TP -\fB\-\-nosubswithbins\fP -Don't subsume with binary clauses. -.TP -\fB\-\-nosubswithnbins\fP -Don't subsume with non-existent binary clauses. -.TP -\fB\-\-noclausevivif\fP -Don't perform clause vivification. -.TP -\fB\-\-nosortwatched\fP -Don't sort watches according to size: bin, tri, etc. -.TP -\fB\-\-nolfminim\fP -Don't do on-the-fly self-subsuming resolution (called 'strong minimisation' in -PrecoSat). -.TP -\fB\-\-nocalcreach\fP -Don't calculate reachability and interfere with variable decisions accordingly. -.TP -\fB\-\-nobxor\fP -Don't find equivalent literals during failed literal search. -.TP -\fB\-\-norecotfssr\fP -Don't perform recursive/transitive OTF self-subsuming resolution. -.TP -\fB\-\-nocacheotfssr\fP -Don't cache 1-level equeue. Less memory used, but disables trans OTFSSR, -adv. clause vivifier, etc. Throw the clause away on backtrack. -.TP -\fB\-\-threads\fP = <\fInum\fP> -Number of threads (default is 1). -.SH "EXIT STATUS" -.PP -The output is a solution, together with some timing information. -The exit status indicates the following: -.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 |