6533b820fe1ef96bd127a1e8
RESEARCH PRODUCT
Attempts to produce minimal Resolution refutations
Olivier Bailleuxsubject
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI]TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESdescription
We address the challenge of searching minimal refutations proofs of inconsistent CNF formulae using the Resolution rule. We propose two algorithms which can only afford formulae of at most 5 variables with a desktop computer. A faster but incomplete algorithm is used to produce "hard" 5 variables 3CNF formulae though a stochastic greedy search. It allowed us to find formulae that can be refuted by producing clauses of at most 3 literals, but whose all minimal refutations contain at least one clause of 4 literals.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2018-01-01 |