Skip to content

Commit

Permalink
Removing confusing sentences
Browse files Browse the repository at this point in the history
  • Loading branch information
msoos committed Jul 20, 2020
1 parent 26109ef commit 9fd591a
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion docs/satcomp20-pdf/ccanr/cms-ccanr.tex
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@
\section{Introduction}
This paper presents the conflict-driven clause-learning (CLDL) SAT solver CryptoMiniSat (\emph{CMS}) augmented with the Stochastic Local Search (SLS)~\cite{DBLP:conf/sat/CaiLS15} solver CCAnr as submitted to SAT Competition 2020.

CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and finely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. It also supports, when compiled as such, to recover XOR constraints and perform Gauss-Jordan elimination on them at every decision level. CryptoMiniSat is authored by Mate Soos.
CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and finely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. CryptoMiniSat is authored by Mate Soos.

CCAnr~\cite{DBLP:conf/sat/CaiLS15} is a stochastic local search (SLS) solver for SAT, which is based on the configuration checking strategy and has good performance on non-random SAT instances. CCAnr switches between two modes: it flips a variable according to the CCA (configuration checking with aspiration) heuristic if any; otherwise, it flips a variable in a random unsatisfied clause (which we refer to as the focused local search mode). The main novelty of CCAnr lies on the greedy heuristic in the focused local search mode, which contributes significantly to its good performance on structured instances

Expand Down
2 changes: 1 addition & 1 deletion docs/satcomp20-pdf/walksat/cms-walksat.tex
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
\section{Introduction}
This paper presents the conflict-driven clause-learning (CLDL) SAT solver CryptoMiniSat (\emph{CMS}) augmented with the Stochastic Local Search (SLS)~\cite{Selman95localsearch} solver WalkSAT v56 as submitted to SAT Competition 2020.

CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and finely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. It also supports, when compiled as such, to recover XOR constraints and perform Gauss-Jordan elimination on them at every decision level. CryptoMiniSat is authored by Mate Soos.
CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and finely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. CryptoMiniSat is authored by Mate Soos.

WalkSAT~\cite{DBLP:conf/aaai/KautzS96} is a standard system to solve satisfiability problems using Stochastic Local Search. The version inside CryptoMiniSat is functionally equivalent to the ``rnovelity'' heuristic of WalkSAT v56 using an adaptive noise heuristic~\cite{DBLP:conf/aaai/Hoos02}. It behaves exactly as WalkSAT with the minor modification of performing early-abort in case the ``lowbad'' statistic (i.e. the quality indicator of the current best solution) indicates the solution is far. In these cases, we early abort, let the CDCL solver work longer to simplify the problem, and come back to WalkSAT later. The only major modification to WalkSAT has been to allow it to import variables and clauses directly from the main solver taking into account assumptions given by the user.

Expand Down

0 comments on commit 9fd591a

Please sign in to comment.