Truth Assignments as Conditional Autarkies

Kiesl, Benjamin and Heule, Marijn J.H. and Biere, Armin
(2019) Truth Assignments as Conditional Autarkies.
In: 17th International Symposium on Automated Technology for Verification and Analysis.
Conference: ATVA - International Symposium on Automated Technology for Verification and Analysis

Full text not available from this repository.

Abstract

An autarky for a formula in propositional logic is a truth assignment that satisfies every clause it touches, i.e., every clause for which the autarky assigns at least one variable. In this paper, we present how conditional autarkies, a generalization of autarkies, give rise to novel preprocessing techniques for SAT solving. We show that conditional autarkies correspond to a new type of redundant clauses, termed globally-blocked clauses, and that the elimination of these clauses can simulate existing circuit-simplification techniques on the CNF level.

Actions

Actions (login required)

View Item View Item