  
1. Extensions of SAT 
 Download your favorite
opensource SAT solver (which does not support the features listed
below) and add the following features:
 Support for PseudoBoolean Constraints (linear constraints
over Boolean variables). For example, in addition to the CNF, the
solver will be able to take as input constraints such as 3x +
2y <= 3, where x,y are Boolean variables
appearing in the CNF formula. The satisfying solution must
satisfy both the CNF constraints and the pseudoBoolean
constraints. Note: there is an exponential way to do this and a
polynomial one  find the polynomial solution.
 AllSAT. Add an option to the SAT solver of getting all
satisfying assignments. Further, allow the user to specify a set
of 'important variables', and find all the solutions that their
projection to this set of variables is distinct.

2. Implement range allocation for equality
logic with SAT 
 Equality logic can be
decided by assigning an adequate finite discrete range of values to
each variable (see Sect. 4.5). Implement a simple version of this
procedure in which each variable has ceiling(log n) bits,
where n is the number of variables, via a reduction to a
propositional formula. Chapter 6 has relevant information about
encoding such bitvector formulas.
As a more advanced project, do the same for a nonuniform range, as
explained in Sects. 4.5.2  4.5.3. 
3. Implement a lazy range allocation for
equality logic inside DPLL(T) 
 Equality logic can be
decided by assigning an adequate finite discrete range of values to
each variable. As in the previous project, encode this range with a
bitvector of the appropriate size. In this project, however,
implement a procedure that generates the clauses for the bitvector
constraints incrementally within DPLL(T). Use unionfind to decide
which constraints need to be added. Compare the performance of your
implementation with the eager encoding using suitable benchmarks.

4. Ondemand Ackermann constraints for
EUF 
 Equality logic with
uninterpreted functions (EUF) can be reduced to equality logic by adding
appropriate Ackermann constraints. The number of constraints can be large,
and may be a burden for the procedure.  Implement a lazy procedure
for adding the Ackermann constraints: If a satisfying assignment is
obtained that violates functional consistency, add those constraints
required to eliminate the assignment, and reiterate.
 Compare the
performance of your implementation with the direct encoding using suitable
benchmarks.

5. Implement Branch & Bound based on
General Simplex. 
 Create an
incremental version of Branch & Bound (Sec. 5.3) based
on general simplex (which is also incremental). This means that given
two similar problem instances, solving them consecutively while
reusing information that was learned during the solving of the first
instance, makes solving the second instance faster. For example,
suppose that the second linear system is equivalent to the first one
except that one of the variables is now required to be integral, and
there was no such requirement in the first system. Obviously we can
do better than just rerunning the solver from scratch.

6. Strict inequalities for the general
simplex algorithm 
 Add support for constraints
with strict inequalities over the reals to the general simplex algorithm
(Sec. 5.2)! 
7. Implement FourierMotzkin and compare
it to Simplex 
 FourierMotzkin can be used to
decide a conjunction of linear constraints over the reals.
 Implement FourierMotzkin for a conjunction of linear constraints.
 Compare the performance of your implementation with a simplex
implementation using suitable benchmarks.

8. Integrating the OMEGA test into
DPLL(T) 
 The OMEGA test is a decision
procedure for a conjunction of linear constraints over the integers, and is
described in Sec. 5.5. Integrate the OMEGA test into DPLL(T)
(Chap. 11) to obtain a decision procedure for linear arithmetic over
the integers with arbitrary Boolean connectives. 
9. Making OMEGA
incremental 
 The OMEGA test, as described
in Sec. 5.5, is not incremental.  Propose and implement an
incremental variant, which should include the possibility to deactivate
constraints.
 Integrate this incremental variant into DPLL(T).
Compare the performance of the nonincremental variant with your new
version.

10. Using DPLL(T) for splitting of the
grey shadow 
 The OMEGA test (Sec. 5.5)
is a recursive procedure. Most of the recursive calls correspond to a
conjunction, that is, if any of the subproblems is unsatisfiable,
so is the original one.
The exception is the grey shadow: it corresponds to a
disjunction, i.e., only if all subproblems are unsatisfiable, so is
the original one. The original OMEGA test performs this
casesplitting inside the algorithm.  Use the propositional
part of DPLL(T) to implement this splitting.
 Compare the performance of both variants using suitable
benchmarks.


11. Compare various circuits for
multipliers for bitvector arithmetic 
 Bitvector arithmetic is
usually decided using a translation into a circuitequivalent. There are
many ways to encode multipliers, to be found in the literature on circuit
construction. Implement and compare a number of variants of multipliers.

12. Build an
SMTfrontend 
 Build an SMTfrontend for a
theory of your choice. Test it using the benchmarks from the SMT
repository. 
13. Build a lazy bitvector
flattener 
 Implement the algorithm
described in Section 6.3. Compare its performance with an eager version of
the algorithm. 
14. Implement the decision procedure for
arrays 
 Implement the algorithm
described in Chapter 7. 
15. Branch & Bound + DPLL(T) for
PseudoBoolean Constraints 
 PseudoBoolean
optimization problems consist of a set of Boolean constraints
(usually in CNF) and a cost function, which associates integer
weights with a subset of the Boolean variables. The goal is to find
the satisfying assignment with the lowest cost. Implement such a
procedure on top of DPLL(T). Use Branch & Bound for the cost
function. 
16. Replacing SAT with
BDDs 
 Replace the SAT solver in
DPLL(T) with a BDD package, and compare the performance. One strength of
BDDs is that they provide inexpensive means to compute projections. What
part of DPLL(T) can leverage this capability? 
17. Modeling: use SAT to solve an IQ test 
 See
here. 
18. Modeling: use PBS or 01 ILP to solve your department's course scheduling
problem 
 See
here. 