Lines Matching refs:solver
2052 option is useful to determine which scopes are tried or which SAT solver is
2092 value greater than 1, you will need an incremental SAT solver, such as
2101 this option to a value greater than 1, you will need an incremental SAT solver,
2181 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
2185 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
2193 Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
2213 \item[\labelitemi] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
2228 \item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in
2236 \item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written
2244 \item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver written in
2252 \item[\labelitemi] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
2266 \item[\labelitemi] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
2276 \textit{smart}, Nitpick selects the first solver among the above that is
2278 Nitpick displays which SAT solver was chosen.
2294 to the SAT solver.
2345 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
2351 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
2752 solver on Windows. Setting the \textit{sat\_solver} option