Prev: Interested in getting good at math any book recommendations?
Next: Convexity of log to sum of exponentials
From: RussellE on 9 Jul 2010 03:20
The HiLo solver is a resolution based counting solver.
It uses DPLL and conflict driven clause learning.
Unlike many solvers, HiLo uses a fixed variable
order and all learnt clauses are of decision variables.

HiLo solvers can start at any position in "assignment space".
The Lo solver counts upward and the Hi solver downward.
This allows parallel solvers to use novel search and restart
strategies. Individual processes can search distinct partitions
of "assignment space" while helping other processes with
relevant learnt clauses.

Assume we order the n variables of a Boolean expression.
Every possible variable assignment can be thought of
as an unique n-bit binary number.

A counting solver tries 0, then 1, then 2, etc.
until a satisfying assignment is found.
This can be really slow when counting by one,
but resolution can be used to count by powers of 2.
Each learnt clause will increment the solver
by some power of 2.
Of course, 1 is a power of two.
This is an important fact for restart strategies.

Types of variables:

free - hasn't been assigned
forced - forced by a unit clause
decision - chosen by solver to be true or false
partition - a special type of forced variable

Lo Counter:

0) Perform unit clause propagation.
1) Assign highest order free variable to false.
2) Perform unit clause propagation.
3) If no conflict go to (1).
4) Learn clause of decision variables.
5) Soft restart.

A soft restart keeps the same variable order
and assumes all variables are free.
Soft restarts are especially important when
other processes may have added learnt clauses.

A hard restart reorders the variables and assumes
all variables are free.

Assume there is a conflict during step 2.
There is an unique unit clause for each forced variable.

(If there is more than one clause forcing a specific
variable, choose the higher order clause.
For example, given (e+c+a) and (d+c+a) where both
clauses force a to be true, choose (e+c+a).)

Let S be the set of these unit clauses and
the conflicting clause(s). Repeatedly resolve
the lowest order forced variable in set S
until only decision variables are left.
The remaining clause is the learnt clause.

This decision clause has the highest order
variables of any of the "conflict" clauses
we can derive. The decision clause
will provide the largest increment for the solver.

The Lo solver will find the lowest numbered
satisfying assignment or derive the empty clause.

The Hi solver is the same as the Lo solver, except
Hi always assumes decision variables are true.
The Hi solver will find the highest numbered
satisfying assignment.

Assume we have a 5-bit (0-31) assignment space and
want to start in the middle. We want to find

SA = satisfying assignment.

Lowest SA >= 16
or
Highest SA <= 15

We do this by making the highest ordered variable,
e, a partition variable.

We add the partition variable(s) as unit clause(s).
Solvers don't share partition clauses and each solver
is given an unique set of partition unit clauses.

In the example above, the Lo solver would add (e) as a
unit clause to find the lowest SA >= 16 and the Hi solver
would add (~e) as a clause to find the highest SA =< 15.

Partition variables are forced. They will be resolved away
when deriving learnt clauses.

The partition has no satisfying assignments
if the empty clause is derived. For example,
if the Lo solver above derives (~e),
we know there is no SA >= 16.

If a SAT instance has many satisfying assignments,
unit clause propagation is likely to find one
quickly regardless of the variable ordering.
If a solution is not found quickly, it is likely
the instance is unsolvable.

The Lo solver has a common method of proving
an instance is unsolvable. The solver will
derive unit clauses for the highest order
variables. Eventually, there will be three
unit clauses contradicting a clause.
For this reason, it is best if all the
highest order variables appear together
in clauses.

A lot of analysis has been done on resolvent
clause size and decision depth.
For counting solvers, the most relevant measure
seems to be variable order depth.

Each learnt clause increments the solver.
If the instance is unsolvable, we don't want the solver
to be incrementing by small values like 2 and 4.
Learnt clauses with low order variables are bad (usually).
We want to do a hard restart if most of the learnt clauses
have low order variables.

What we really want to know is the "toggle rate".
How often is a specific variable changing
from a decision variable to a forced variable?
Some variable toggles every time a learnt clause is added.

The variable ordering determines how many times a variable
can toggle. The highest order variable can only toggle once.
The second highest order variable can toggle no more than twice.
The lowest order variable can toggle as many as 2^(n-1) times.

The lowest order variable in a learnt clause can
only toggle (go back to a decision variable)
if a higher order variable in the learnt clause toggles.

We can now define a "toggle rating" for each variable.
A variable only has a toggle rating if the variable
is the lowest order variable in a learnt clause.

The toggle rating of a variable is equal to the
"position constant" of the second lowest order
variable in the learnt clause.

The position constant is 2^(n-i-1) for the i'th position
where 0 is the lowest position and n-1 the highest.

For example, assume we have 5 variables: e,d,c,b,a
and a learnt clause (e+c+b). Variable c is the second
lowest variable in the clause and has position 2.
The toggle rating for variable b is 2^(5-2-1) = 4.

The clause (e+c+b) can make b toggle no more than
four times. Variable b can only toggle if e or c
toggle. Because of it's position in the order,
variable c can toggle, at most, four times.

We want to do a hard restart if low order
variables have high toggle ratings.
The highest order variables in the new order
should be variables with high toggle ratings.


Russell
- 2 many 2 count
From: RussellE on 9 Jul 2010 21:34
On Jul 9, 12:20 am, RussellE <reaste...(a)gmail.com> wrote:

> Partition variables are forced. They will be resolved away
> when deriving learnt clauses.

Sorry, this is incorrect.
Partition variables should be treated as decision variables.
Partition variables can appear in learnt clauses.
If a process's partition variables contradict a learnt clause,
the partition for that process has no satsifying assignments.
 | 
Pages: 1
Prev: Interested in getting good at math any book recommendations?
Next: Convexity of log to sum of exponentials