Clause Learning and P-Optimality Revisited

by Ahmed and Christine and Daniel and Karl

algebraic and logic methods we cover:
-- polynomial methods
-- combinatoric methods

for maybe pathway analysis and design or ...

Some thirty 30 years ago the last author developed
a non-chronological backtracking technique
based on clause learning (called superresolution)
which has been reinvented and
incorporated in most competitive SAT solvers.
Some 25 years ago, the second author was involved in the development
of P-optimal biased-coin-flipping algorithms
for Generalized Satisfiability.
In the last 25 years the importance of SAT solvers has grown significantly
and they are now used in numerous application domains.

In this paper we bring together, for the first time,
clause learning and P-optimal algorithms
and we demonstrate the usefulness of this
integration on a benchmark.

An important attraction of this work is that we can show that
our polynomial-time algorithms are P-optimal
in the following sense: they guarantee a performance ratio t[R]
(0<= t[R] <= 1), where R
is a subset of the 256 binary relations of rank 3 and if we could raise
the performance ratio to t[R] + 1/trillionth still with a
polynomial-time algorithm, then P=NP.
For example, if R contains one element namely the OneInThree relation, then
t[R] = 4/9.
None of the algorithms that have been considered before in the SAT and CSP
communities have this property.

In 2003, Kautz and Selman posed several challenges to the SAT community,
including:

CHALLENGE 3A:
Demonstrate that a propositional proof system more powerful
than tree-like resolution can be made practical
for satisfiability testing.

We reintroduce a propositional proof system that
is more powerful than tree-like resolution and that is practical.
It was known in 1975 as algorithm Rj in an ETH Zurich Technical Report

http://www.ccs.neu.edu/research/demeter/biblio/clause-learning0.html

and in 1977 as an abstract in the American Mathematical Society,
as superresolution.

http://www.ccs.neu.edu/research/demeter/biblio/clause-learning.html

It was shown in the 1977 paper that SuperResolution and Resolution
are polynomially equivalent.

Similar results were obtained 20 years later:

Kautz and Selman write:
...
They further showed that
combining clause learning with restarts [52, 53] (where learned clauses are     \
saved
between restarts) is equivalent to general resolution.

52. Carla P. Gomes, Bart Selman, and Henry Kautz. Boosting Combinatorial Search
Through Randomization. In Proc. 15th Natl. Conf. on Artificial Intelligence
(AAAI-98), pages 431?438, 1998.
53. Luis Baptista and Joao P. Marques Silva. Using randomization and learning to
solve hard real-world instances of satisfiability. In Prin. and Prac. of Const.     \
Prog.,
pages 489?494, 2000.

Contents:

1.  Introduction
1.1 Motivating example
    (showing the polynomials and clause
    learning in action (from poster).)
1.2 paper organization

2.  Relation primitives
    We need the relation primitives both for the
    transition system and for biased coins.
      forced variables
      relation reduction
      effective variables
      subsumption

3. Transition system for MaxCSP
3.1 Superresolution
3.1.1 Optimized Superresolution (is this the same as
      normal super resolution from my 1977 paper?)
3.2 SAT
Transition system for SAT to explain superresolution
3.3 MaxSAT
Transition system for MaxSAT based on superresolution
3.4
Transition system for MaxCSP based on superresolution

4. From fair to optimally biased coins
4.1 Derandomization

5. Integrating Superresolution and optimally biased coins

Variations:
Value ordering
Variable ordering

6. Implementation

7. Experimental results

I still think a good organization neatly separating the concerns
is possible.