On conversions from CNF to ANF

DOI10.1016/j.jsc.2019.07.023zbMath1432.68600OpenAlexW2964724182MaRDI QIDQ2307626

Martin Kreuzer, Jan Horáček

Publication date: 24 March 2020

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2019.07.023

zbMATH Keywords

resolutionSAT solvingBoolean polynomialalgebraic normal formconjunctive normal formBoolean Gröbner basis

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Boolean functions (06E30) Boolean functions (94D10) Computational aspects of satisfiability (68R07)

Related Items (1)

Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions

Uses Software

• FGb
• Magma
• PolyBoRi
• SageMath
• ApCoCoA
• Glucose
• CryptoMiniSat
• antom
• CNFgen
• Bosphorus

Cites Work

• Refutational theorem proving using term-rewriting systems
• Resolution over linear equations and multilinear proofs
• Polybori: A framework for Gröbner-basis computations with Boolean polynomials
• The Magma algebra system. I: The user language
• Lower Bounds for Splittings by Linear Combinations
• Algebraic attacks using SAT-solvers
• Algebraic Cryptanalysis
• Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases
• Integrating Algebraic and SAT Solvers
• ElimLin Algorithm Revisited
• FGb: A Library for Computing Gröbner Bases
• A Gröbner Basis Approach to CNF-Formulae Preprocessing
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On conversions from CNF to ANF