To enhance user privacy, anonymous credential systems allow the user to convince a verifier of the possession of a certificate issued by the issuing authority anonymously. In the systems, the user can prove relations on his/her attributes embedded into the certificate. Previously, a pairing-based anonymous credential system with constant-size proofs in the number of attributes of the user was proposed. This system supports the proofs of the inner product relations on attributes, and thus can handle the complex logical relations on attributes as the CNF and DNF formulas. However this system suffers from the computational cost: The proof generation needs exponentiations depending on the number of the literals in OR relations. In this paper, we propose a pairing-based anonymous credential system with the constant-size proofs for CNF formulas and the more efficient proof generation. In the proposed system, the proof generation needs only multiplications depending on the number of literals, and thus it is more efficient than the previously proposed system. The key of our construction is to use an extended accumulator, by which we can verify that multiple attributes are included in multiple sets, all at once. This leads to the verification of CNF formulas on attributes. Since the accumulator is mainly calculated by multiplications, we achieve the better computational costs.

The number of satisfying assignments of k-CNF formulas is computed using the inclusion-exclusion formula for sets of clauses. Recently, it was shown that the information on the sets of clauses of size log k + 2 already uniquely determines the number of satisfying assignments of k-CNF formulas. The proof was, however, only existential and no explicit procedure was presented. In this paper, we show that such a procedure exists.

In this paper, we consider two types of promises for (k-)CNF formulas which can help to find a satisfying assignment of a given formula. The first promise is the Hamming distance between truth assignments. Namely, we know in advance that a k-CNF formula with n variables, if satisfiable, has a satisfying assignment with at most pn variables set to 1. Then we ask whether or not the formula is satisfiable. It is shown that for k 3 and (i) when p=nc (-1 < c 0), the problem is NP-hard; and (ii) when p=log n/n, there exists a polynomial-time deterministic algorithm. The algorithm is based on the exponential-time algorithm recently presented by Schoning. It is also applied for coloring k-uniform hypergraphs. The other promise is the number of satisfying assignments. For a CNF formula having 2n/2nε (0 ε < 1) satisfying assignments, we present a subexponential-time deterministic algorithm based on the inclusion-exclusion formula.