To propose a link enter your email address:

and
 
 
 

Deadline Countdown

 
 

Heads up on SAT research

 
 

SAT related books

 
 

Other SAT related sites

SATLIB: the satisfiability library
SAT-Ex: experimentations about SAT
QBFLIB: the QBF library
PBLIB: The pseudo-boolean library
SMTLIB: The Satisfiability Modulo Theory library
SAT4J:A SATisfiability library for Java
 

 

Show   all the links
only papers
   containing the keyword:     ordered by:  date
hits
Show all

3 elements available
 
  
Date:11-Jan-2012
Title:Call for Papers - IWSBP 2012
Hits:221
Contributed by: Miroslav Velev
Keywords:Repository, Verification, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Instance simplification, Satisfiable Problems Generation, SAT tools, call for papers, null, null
 
  
 
Call for Papers - IWSBP 2012

-------------------------------------------------------------------------

Please, feel free to forward this message to interested people.
We apologize if you receive this email more than once.

-------------------------------------------------------------------------


Dear colleague,

the 10th International Workshop on Boolean Problems will be held on
     September 19-21, 2012, in Freiberg, Germany.

More information you can find on the workshop web page 
     http://www.informatik.tu-freiberg.de/prof2/ws_bp10/

Deadlines
     Submission - May 5, 2012
     Acceptance notices - June 9, 2012
     Final version submission - July 7, 2012

Sincerely,
Prof. Dr.-Ing. habil. Bernd Steinbach

Call for Papers

The workshop on Boolean problems has an emphasis on the problems related to the solution of all kinds 
of high-dimension Boolean and discrete problems, and provides a forum for researchers and engineers 
from different disciplines to exchange ideas. The workshop is devoted to theoretical discoveries as well as 
practical applications. An aim of the workshop is to initiate possible collaborative research and to find 
new areas of application. It is intended to publish the papers in proceedings. The invited speakers
 - Mitch Thornton (SMU Dallas (Texas), USA),
 - Raimund Ubar (TTU Tallinn, Estonia), and
 - Vincent Gaudet (University of Waterloo, Canada) are presenting essential results of their research. 

Topics of interest (not limited to)

     Theory
        Properties and applications of Boolean Algebras
     Data Structures and Algorithms
        Modeling
        Specification of data structures/algorithms
        Complexity
     Program Systems/Software
        Fundamental software for the solution of Boolean Problems
        Comparison of efficiency
     Practical Applications
        Application of Boolean algebra in FPGA synthesis  
        Quantum logic, reversible logic, and multi-valued logic
        Solution of real-world problems

Submissions

To submit a paper, please send an extended abstract, no longer than 6 pages, as a PDF file to 

iwsbp2012@informatik.tu-freiberg.de 

or using the workshop web page 

http://www.informatik.tu-freiberg.de/prof2/ws_bp10/ 

by April 25, 2012. Acceptance notices will be sent by June 9, 2012. 
The final version of the paper should be submitted by July 7, 2012.

Program Committee
- J. Butler, Naval Postgraduate School Monterey, USA
- R. Berghammer, C-A-University of Kiel, Germany
- L. Cheremisinova, Minsk Academy of Science, Belarus
- D. Debnath, Oakland University, USA
- R. Drechsler, University of Bremen, Germany
- E. Dubrova, Royal Institute of Technology (KTH), Sweden
- G. Dueck, University of New Brunswick, Canada
- D. Große , University of Bremen, Germany
- I. Levin, Tel Aviv University, Israel
- T. Luba, Warsaw University of Technology, Poland
- M. Miller, University of Victoria, Canada
- C. Moraga, TU Dortmund, Germany
- M. A. Perkowski, Portland State University, USA
- Y. Pottosin, Minsk Academy of Science, Belarus
- T. Sasao, Kyushu Institute of Technology, Japan
- Ch. Scholl, University of Freiburg, Germany
- R. Stankovic, University of Nis, Serbia
- B. Steinbach, University of Freiberg, Germany
- R. Ubar, Tallinn Technical University, Estonia
- M. Velev, Aries Design Automation, USA
- A. De Vos, University of Gent, Belgium
- S. Yanushkevich, University of Calgary, Canada
- A. D. Zakrewskij, Minsk Academy of Science, Belarus

Conference Language: English

Conference Location: Freiberg University of Mining and Technology, Freiberg (Sachs.), Germany
 
 
 

 
  
Date:19-Feb-2011
Title:verified-unsat track of sat 2011 competition
Hits:718
Contributed by: Van Gelder, Allen
Keywords:Verification, QBF, SAT tools, SAT-Solver Competition, Resolution proof, null
 
  
 

In the verified-unsat track of the 2011 Sat Solver Competition, solvers produce some verification output and are only tested on unsatisfiable benchmarks.

NEW THIS YEAR: We accept submission of QBF solvers that produce certificates and we accept verification tools for both SAT and QBF.

Because the verification track is very experimental, I will be more flexible than the main tracks about the forms of submission. There are several accepted proof formats, each with precise specifications. All formats may be found at http://www.cse.ucsc.edu/~avg/ProofChecker/.

fileformat_qir.txt

fileformat_rup.txt

ProofChecker-fileformat.txt

These formats are designed to be neutral to the solver's methodology as far as possible but RUP and QIR are most natural for CDCL-style solvers that employ the grasp/chaff/minisat paradigm.

The new QIR format works for Q-resolution proofs in clausal QBF and resolution proofs in SAT. The others are SAT only. The QIR format achieves the twin goals of accepting proofs that are compact and having a proof language that is recognizable in deterministic log space.

 
 
 

 
  
Date:25-Oct-2007
Title:Announcing Z3 Version 1.1
Hits:1985
Contributed by: Leonardo de Moura
Keywords:Verification, SAT tools, SAT-Based, Satisfiability Modulo Theory, SAT-solver, null, null, null
 
  
 

We are pleased to announce of Z3 version 1.1.

Z3 is a new high-performance theorem prover for Satisfiability Modulo Theories (SMT) problems being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 has already been integrated in several projects and products at Microsoft. It can read problems in SMT-LIB, Simplify and a native low-level format. Z3 can also be invoked programmatically from either C/C++, OCaml or from .NET.

More information about Z3, including download links are available from:

http://research.microsoft.com/projects/z3

Kind regards,
Leonardo de Moura and Nikolaj Bjorner.

 
 
 

 

© 2000-2001 Business & Technology Research Laboratory. © 2001-2005 Centre de Recherche en Informatique de Lens. Hosted by Innovation and Technology Research Lab. Please send any comment to daniel@satlive.org.