STRUCTure is build on top of Constellation which is a framework for distributed application. In Constellation you have activities that perform your tasks. Each activity can spawn and communicate with other activities provided that the identifiers are known. There is no distributed shared memory and an activity can be run on any participating machine. With this in mind let us see the design of STRUCTure.
STRUCTure is a DPLL type algorithm. It is not conflict-driven and doesn't learn new clauses. Let's say we have a SAT formula (usually in CNF), F. On F we can apply different reasonings such as
- equivalent literals.
- contradictory literals.
- transitivity.
- pure literals.
- units propagation.
- hyper binary resolution.
- sub-summing.
- self-sub-summing (currently one clause is a binary).
After the formula was simplified we have three options.
- All literals were assigned and thus F is satisfiable.
- A contradiction (e.g. F contains an empty clause) was found and thus F is unsatisfiable.
- No solution was found and thus F is unknown.
If the formula F is unknown we can pick a literal a and branch on a, i.e. we try to solve children formula F- = {-a} ∧ F and F+ = {a} ∧ F.
- if F- and F+ and unsatisfiable then F is unsatisfiable.
- else if F- or F+ are satisfiable then F is satisfiable with solution given by the satisfied children.
- else F is unknown (sometimes, e.g. maximum depth was reached, we can just return unknown without branching).
The performance of STRUCTure can be seen in the next image. The program was run on DAS-4 against SAT09 competition medium-level instances with a time limit of 600s on 8 cores.
No comments:
Post a Comment