Sciweavers

JSAT
2010
130views more  JSAT 2010»
13 years 5 months ago
DepQBF: A Dependency-Aware QBF Solver
We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quan...
Florian Lonsing, Armin Biere
JAL
2000
82views more  JAL 2000»
13 years 10 months ago
New Upper Bounds for Maximum Satisfiability
The (unweighted) Maximum Satisfiability problem (MaxSat) is: given a boolean formula in conjunctive normal form, find a truth assignment that satisfies the most number of clauses....
Rolf Niedermeier, Peter Rossmanith
ECCC
2000
77views more  ECCC 2000»
13 years 10 months ago
Polynomial-Time Recognition of Minimal Unsatisfiable Formulas with Fixed Clause-Variable Difference
A formula (in conjunctive normal form) is said to be minimal unsatisfiable if it is unsatisfiable and deleting any clause makes it satisfiable. The deficiency of a formula is the ...
Herbert Fleischner, Stefan Szeider
JSAT
2006
87views more  JSAT 2006»
13 years 10 months ago
Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques
A family of satisfiable benchmark instances in conjunctive normal form is introduced. The instances are constructed by transforming a random regular graph into a system of linear ...
Harri Haanpää, Matti Järvisalo, Pet...
JSAT
2006
119views more  JSAT 2006»
13 years 10 months ago
A Faster Clause-Shortening Algorithm for SAT with No Restriction on Clause Length
We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. This algorithm uses the clauseshorte...
Evgeny Dantsin, Alexander Wolpert
JAIR
2006
106views more  JAIR 2006»
13 years 10 months ago
Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas
Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable for...
Enrico Giunchiglia, Massimo Narizzano, Armando Tac...
FCS
2006
14 years 6 days ago
The Representational Power of Conjunctive Normal Form
- There is continuing research interest in comparison of the complexity of problems within the class NP-Complete. This paper examines the representational power of conjunctive norm...
Thomas O'Neil, Jason Smith
ECAI
2008
Springer
14 years 17 days ago
New Results for Horn Cores and Envelopes of Horn Disjunctions
We provide a characterization of Horn cores for formulas in conjunctive normal form (CNF) and, based on it, a novel algorithm for computing Horn cores of disjunctions of Horn CNFs ...
Thomas Eiter, Kazuhisa Makino
ECAI
2008
Springer
14 years 17 days ago
Vivifying Propositional Clausal Formulae
Abstract. In this paper, we present a new way to preprocess Boolean formulae in Conjunctive Normal Form (CNF). In contrast to most of the current pre-processing techniques, our app...
Cédric Piette, Youssef Hamadi, Lakhdar Sais
FUZZIEEE
2007
IEEE
14 years 18 days ago
Consistent, Complete and Compact Generation of DNF-type Fuzzy Rules by a Pittsburgh-style Genetic Algorithm
When a flexible fuzzy rule structure such as those with antecedent in conjunctive normal form is used, the interpretability of the obtained fuzzy model is significantly improved. H...
Jorge Casillas, Pedro Martínez