Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using SMT-solving techniques, which combine SAT-solving with decision procedures for conjunctions and propagation techniques.
Formulele cu negații, conjuncții și disjuncții combină dificultățile testării satisfiabilității cu cele ale deciziei conjuncțiilor; ele sunt, în general, decise astăzi folosind tehnici de rezolvare SMT⁠(d), care combina rezolvările SAT cu procedurile de decizie pentru conjuncții și tehnici de propagare.