From 82ef9f4530b1192b5e7db43a4ca4769b9cac60e6 Mon Sep 17 00:00:00 2001 From: Lars Tveito Date: Thu, 21 Nov 2019 14:56:51 +0100 Subject: [PATCH] Small correction --- committees.org | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/committees.org b/committees.org index 4efc771..112b6ef 100644 --- a/committees.org +++ b/committees.org @@ -609,9 +609,9 @@ using SMT-solving. ** When not to use SMT SAT is an NP-complete problem, and solving for richer theories does not - reduce this complexity. So in general, SMT solving is NP-complete and not - even decidable in all cases. If you are presented with a problem that has a - known polynomial algorithm, then don't use an SMT solver. + reduce this complexity. So in general, SMT solving is NP-hard and not even + decidable in all cases. If you are presented with a problem that has a known + polynomial algorithm, then don't use an SMT solver. It is important to try to compartmentalize your SMT-instances; solving many small SMT-instances is likely to be more efficient than solving one large.