Sciweavers

CP
2010
Springer
13 years 2 months ago
Computing the Density of States of Boolean Formulas
Abstract. In this paper we consider the problem of computing the density of states of a Boolean formula in CNF, a generalization of both MAX-SAT and model counting. Given a Boolean...
Stefano Ermon, Carla P. Gomes, Bart Selman
JAL
2000
82views more  JAL 2000»
13 years 4 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
JSAT
2006
91views more  JSAT 2006»
13 years 4 months ago
Extending Existential Quantification in Conjunctions of BDDs
Abstract. We introduce new approaches intended to speed up determining the satisfiability of a given Boolean formula expressed as a conjunction of Boolean functions. A common prac...
Sean Weaver, John V. Franco, John S. Schlipf
CORR
2008
Springer
124views Education» more  CORR 2008»
13 years 4 months ago
A New Upper Bound for Max-2-Sat: A Graph-Theoretic Approach
In MaxSat, we ask for an assignment which satisfies the maximum number of clauses for a boolean formula in CNF. We present an algorithm yielding a run time upper bound of O (2 K 6....
Daniel Raible, Henning Fernau
STOC
1987
ACM
104views Algorithms» more  STOC 1987»
13 years 7 months ago
The Boolean Formula Value Problem Is in ALOGTIME
The Boolean formula value problem is in alternating log time and, more generally, parenthesis context-free languages are in alternating log time. The evaluation of reverse Polish ...
Samuel R. Buss
FROCOS
2009
Springer
13 years 8 months ago
Efficient Combination of Decision Procedures for MUS Computation
In recent years, the problem of extracting a MUS (Minimal Unsatisfiable Subformula) from an unsatisfiable CNF has received much attention. Indeed, when a Boolean formula is proved ...
Cédric Piette, Youssef Hamadi, Lakhdar Sais
FOCS
2006
IEEE
13 years 10 months ago
Succinct Non-Interactive Zero-Knowledge Proofs with Preprocessing for LOGSNP
Let Λ : {0, 1}n ×{0, 1}m → {0, 1} be a Boolean formula of size d, or more generally, an arithmetic circuit of degree d, known to both Alice and Bob, and let y ∈ {0, 1}m be a...
Yael Tauman Kalai, Ran Raz
ICALP
2009
Springer
14 years 4 months ago
Limiting Negations in Formulas
Negation-limited circuits have been studied as a circuit model between general circuits and monotone circuits. In this paper, we consider limiting negations in formulas. The minimu...
Hiroki Morizumi