larstvei/SMT-for-IN3070
1
0
Fork 0
mirror of https://github.com/larstvei/SMT-for-IN3070.git synced 2024-11-26 03:28:31 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Small correction

Browse Source
This commit is contained in:
Lars Tveito 2019-11-21 14:56:51 +01:00
parent bb3f43e198
commit 82ef9f4530
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
committees.org
View File

@ -609,9 +609,9 @@ using SMT-solving.
** When not to use SMT ** When not to use SMT
SAT is an NP-complete problem, and solving for richer theories does not 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 reduce this complexity. So in general, SMT solving is NP-hard and not even
even decidable in all cases. If you are presented with a problem that has a decidable in all cases. If you are presented with a problem that has a known
known polynomial algorithm, then don't use an SMT solver. polynomial algorithm, then don't use an SMT solver.
It is important to try to compartmentalize your SMT-instances; solving many 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. small SMT-instances is likely to be more efficient than solving one large.