(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
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Cas Cremers (CC) |
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Benjamin Kiesl |
| Date Deposited: | 09 Dec 2019 14:29 |
| Last Modified: | 18 Jun 2020 09:27 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2999 |
Actions
Actions (login required)
 |
View Item |