Quick wordsmith

README.md

@@ -129,7 +129,7 @@ that too:
     #demand guilt _ is guilty.
 
 Answer set programming is sometimes compared to boolean satisfiability solving, and is sometimes
-implemented with, general purpose satisfiablity solvers. We can also use Dusa as a pretty bad boolean
+implemented with general purpose satisfiablity solvers. We can also use Dusa as a (pretty bad) boolean
 satisfibility solver, by assigning every proposition we come across the value `true` or `false`. The
 [Wikipedia article describing a basic SAT-solving algorithm, DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm),
 uses as its example the following SAT instance:
@@ -140,7 +140,8 @@ uses as its example the following SAT instance:
     (a' + b  + c') * (a' + b' + c )
 
 We can ask Dusa to solve this problem by negating all the OR-ed together clauses and making them
-`#forbid` constraints.
+`#forbid` constraints — needing one of the literals in the clause to hold is the same as needing
+all of their negations to hold.
 
     a is { true, false }.
     b is { true, false }.