This page is designed to
help you explore the single watched literal algorithm (two watched
literals coming soon). Hover over any of the buttons, or the boxes outlined in red, for
quick instructions.
In the first box you can enter new
clauses. The atoms and clauses will appear in the boxes below.
The second box shows the valuation of each atom, together with two
colums shoing the numbers of negative and positive watched literals
for that atom. If the value of the stom is set, then the cell showing
the number of literals contradicted by that value is shown in red.
The third box shows the clauses,
with a watched literal shown by a black border. If a watched literal
violates the invariant it will be coloured red.
The step button
steps through an
automated search for a solution, and
logs the search steps so you can examine them at leisure.
type new clauses here:
hit return or tab to enter.