Abstract. This paper shows that idempotents in finite rings of integers can act as Generalized Boolean Assignments (GBA’s) by providing a completeness theorem. We introduce the ...
In this paper we introduce MINIMAXSAT, a new Max-SAT solver that incorporates the best SAT and Max-SAT techniques. It can handle hard clauses (clauses of mandatory satisfaction as ...
Abstract. A promising approach for model counting was recently introduced, which in theory requires the use of large random xor or parity constraints to obtain near-exact counts of...
Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most ...
In this paper a new circuit sat based encoding of boolean formula is proposed. It makes an original use of the concept of restrictive models introduced by Boufkhad to polynomially ...
We first define a mapping from CSP to many-valued SAT which allows to solve CSP instances with many-valued SAT solvers. Second, we define a new many-valued resolution rule and p...
Unmanned aerial vehicles (UAVs) represent an important class of networked robotic applications that must be both highly dependable and autonomous. This paper addresses sensor deplo...