• Proteus

  • Referenced in 11 articles [sw10080]
  • recent years, portfolio approaches to solving SAT problems and CSPs have become increasingly common. There ... number of different encodings for representing CSPs as SAT instances. In this paper, we leverage ... problem instance into SAT, selecting an appropriate encoding and a corresponding SAT solver. Our experimental ... that involved four CSP solvers, three SAT encodings, and six SAT solvers, evaluated...
  • CCLS

  • Referenced in 20 articles [sw36049]
  • version, has extensive applications. Weighted MAX-SAT instances encoded from real-world applications ... exist on SLS algorithms for weighted MAX-SAT. In this paper, we propose...
  • MUP

  • Referenced in 15 articles [sw11910]
  • After establishing the unsatisfiability of a SAT instance encoding a typical design task, there...
  • Transalg

  • Referenced in 5 articles [sw17349]
  • Transalg system, designed to produce SAT encodings for discrete functions, written as programs ... such programs to SAT is based on propositional encoding methods for formal computing models ... used the Transalg system to make SAT encodings for a number of cryptographic functions...
  • Azucar

  • Referenced in 5 articles [sw10083]
  • Solver Using Compact Order Encoding. This paper describes a SAT-based CSP solver Azucar. Azucar ... solves a finite CSP by encoding it into a SAT instance using the compact ... order encoding and then solving the encoded SAT instance with an external SAT solver ... order encoding. Azucar is developed as a new version of an award-winning SAT-based...
  • Sugar

  • Referenced in 27 articles [sw09758]
  • SAT-based Constraint Solver. Constraint Satisfaction Problem (CSP) is encoded to a Boolean CNF formula...
  • SATLIB Benchmark Suite

  • Referenced in 3 articles [sw11916]
  • uniform Random-3-SAT; test-sets obtained by encoding ... instances from random instance distribution of SAT-encoded combinatorial problems such as Graph Colouring ... individual SAT-encoded instances from various domains. The majority of the instances from the benchmark ... search algorithms for SAT. For the SAT-encoded problems, the hardness of the instances...
  • Picat-SAT

  • Referenced in 3 articles [sw21859]
  • power of SAT solvers, a SAT compiler must encode domain variables and constraints into ... formula. Despite many proposals for SAT encodings, there are few working SAT compilers. This paper ... Picat system. Picat-SAT employs the sign-and-magnitude log encoding for domain variables...
  • Scarab

  • Referenced in 3 articles [sw07397]
  • which is a prototyping tool for developing SAT-based systems. It provides a rich constraint ... constraints, and all of them are encoded into SAT ... without the need of developing dedicated encoder. SAT solvers are then used for finding solutions...
  • RP-DeLP

  • Referenced in 4 articles [sw19192]
  • scalable implementation of this algorithm using SAT encodings, and we provide an experimental evaluation when...
  • meSAT

  • Referenced in 5 articles [sw29642]
  • meSAT: multiple encodings of CSP to SAT. One approach for solving Constraint Satisfaction Problems ... reduction to propositional satisfiability problem (SAT). A number of encodings (e.g., direct, log, support, order ... linear CSP problems into SAT instances using several well-known encodings, and their combinations...
  • PySAT

  • Referenced in 18 articles [sw25459]
  • SAT oracles and also integrates a number of cardinality constraint encodings, all aiming at simplifying...
  • MathCheck

  • Referenced in 13 articles [sw13642]
  • space of the SAT solver, by providing learned clauses that encode theory-specific lemmas ... addition, the combination enables a more efficient encoding of problems than a pure Boolean representation ... them have failed until now. Using our SAT+CAS system, MathCheck, we extend these...
  • BEE

  • Referenced in 8 articles [sw16989]
  • SAT with BEE. We present BEE, a compiler which enables to encode finite domain constraint ... various possible CNF encodings. Often, the better encoding choice is made after constraint simplification ... Prolog and integrates directly with a SAT solver through a suitable Prolog interface. We demonstrate...
  • SatELite

  • Referenced in 1 article [sw31322]
  • particularly aimed at improving SAT encodings resulting from translation of netlists (combinational boolean circuits). With ... three industrial categories in the SAT 2005 competition. The stand-alone MiniSat took...
  • PaSAT

  • Referenced in 4 articles [sw41090]
  • implementation is on speeding up SAT-checking of propositional encodings of real-world combinatorial problems...
  • CoReS

  • Referenced in 4 articles [sw28116]
  • CoReS}, we automatically encode all required properties into SAT- and SMT-formulas to iteratively compute ... results to evaluate and compare the two encoding approaches...
  • npSolver

  • Referenced in 1 article [sw13580]
  • pseudo-Boolean (PB) solver npSolver encodes PB into SAT and solves the optimization instances ... translate PB to SAT based on a portfolio of different encodings, based on the number...
  • Bloqqer

  • Referenced in 31 articles [sw09578]
  • represented. However, the translation to processable QBF encodings is in general not unique ... elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows...
  • countAntom

  • Referenced in 2 articles [sw40124]
  • provide the following #SAT specific benchmark collection: Fault Injection: Encode the probability of a successful...