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

28 elements available
 
  
Date:03-Apr-2010
Title:KR 2010
Hits:217
Contributed by: Anonymous
Keywords:Computational logic, Logic, General Interest, null, null
 
  
 

Please join us for the Twelfth International Conference on the Principles of Knowledge Representation and Reasoning (KR 2010), to be held May 9-13, 2010 at The Sutton Place Hotel, in Toronto, Ontario, Canada.

The deadline for registration is April 9th!

KR 2010 will be co-located with AAMAS, FOIS, ICAPS, and NMR. Options for cross-registration are available.

 
 
 

 
  
Date:01-Mar-2010
Title:Postdoctoral and senior researcher positions in computing research
Hits:219
Contributed by: Ilkka Niemela
Keywords:Computational logic, SAT/CP Integration, Answer Set Programming, null
 
  
 
Helsinki Institute for Information Technology HIIT and the Aalto University Department of Information and Computer Science are inviting applications for postdoctoral and senior researcher positions in several areas of computing research including: machine learning and data analysis; computational methods for networks, interaction and economics; large constraint models; nanoscale self-assembly; enhancement of internet infrastructure; human-centric ubiquitous IT.

The closing date for applications is 15 March 2010. The positions will be filled for three years maximum starting at the earliest 1 August 2010.

Further details of the posts and the application procedure are available at:
http://www.hiit.fi/jobs (3 positions)
http://ics.tkk.fi/en/vacancies/ (4 positions)

SAT related, in particular, a position on

Constructing and Solving Large Constraint Models

See, http://research.ics.tkk.fi/calls/postdocs2010/

 
 
 

 
  
Date:25-Jan-2010
Title:LoCoCo 2010 -- Workshop on Logics for Component Configuration
Hits:245
Contributed by: Inês Lynce
Keywords:Computational logic, Benchmark, SAT application, null
 
  
 

Workshop of SAT at FLoC 2010, Edinburgh, Scotland, July 10, 2010
First Call for Papers
                           
Scope:
====== 
Modern software distributions are based on the notion of components, which
denote units of independent development and deployment. Components provide
the necessary flexibility when organizing a complex software distribution,
but also are a challenge when it comes to selecting components from a large
repository of possible choices, and configuring these components according
to user needs, resource constraints, and interdependencies with other
components.  Representing and solving configuration problems is a hot topic
of great importance for many application domains. Some well-known examples
of complex systems of components in the world of Free and Open Source
software are the different distributions for GNU/Linux, BSD, or Eclipse
plugins.

Understanding and solving these questions is an attractive research
topic since the problems to be solved are complex and interesting for
researchers working on solving techniques, and on the other hand have
the potential of high impact on the way the software we all use
everyday is developed and deployed. Not only adequate logical
formalisms to represent a configuration problem are required, but also
sophisticated reasoning technologies to deal with large amounts of
data. Further relevant aspects include diagnosis of failed
configuration settings and an intelligent behavior dealing with user
preferences.

This workshop will focus on logic-based methods for specifying and solving
complex configuration problems for software components.  The goal of the
workshop is to bring together both researchers and practitioners active in
the area of component configuration of software systems, using different
modeling and solving techniques, such as constraint and logic programming,
description logics, satisfiability and its extensions. The workshop will be
an opportunity to discuss common and complementary solutions for solving
component configuration.

Invited Talk
============ 
An invited talk will be given by Carsten Sinz (University of Karlsruhe).

MISC 2010
========= 
The first Mancoosi International Solver Competition will be held in
conjunction with the LoCoCo workshop.

Important Dates 
=============== 
Friday, March 26   Submission deadline 
Friday, April 23   Notification about acceptance 
Friday, May 21     Final paper due
Saturday, July 10  Workshop

Submission and Publication 
========================== 
We welcome submissions of various types of presentations related to
the topics of the workshop, such as 
- full research papers
- abstracts of ongoing work 
- tutorial overview papers 
- summaries of research projects 
- system descriptions, if possible including system demonstration at the
  workshop. These must provide the means to download and evaluate the
  system, with preference to distribution under an open source licence.

Program Committee
================= 
Daniel Le Berre (Universite d'Artois, France)
Roberto Di Cosmo (Universite Paris-Diderot, France)
Georg Gottlob (Oxford University, UK)
Pascal van Hentenryck (Brown University, USA)
Matti Jarvisalo (University of Helsinki, Finland)
Ines Lynce (INESC-ID, Lisbon, Portugal), co-chair
Toni Mancini (Sapienza Universita di Roma, Italy)
Albert Oliveras (Technical University of Catalonia, Barcelona, Spain)
Christian Schulte (KTH, Stockholm, Sweden)
Ralf Treinen (Universite Paris-Diderot, France), co-chair
Nic Wilson (UCC, Cork, Irland)
 
 
 

 
  
Date:14-Sep-2008
Title:special issue of AMAI on CFVAI
Hits:871
Contributed by: Miroslav Velev
Keywords:Computational logic, Verification, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, SAT tools, call for papers
 
  
 
Dear Colleague, We would like to invite you to submit a paper to the special issue of Annals of Mathematics and Artificial Intelligence (AMAI) on the topic of application of Constraints to Formal Verification and AI (CFVAI). The submission deadline is November 20, 2008. Topics include, but are not limited to, the following: - application of constraint solvers to hardware verification; - application of constraint solvers to software verification; - dedicated solvers for formal verification problems; - tuning SAT for formal verification and testing; - scheduling, and planning; - challenging formal verification, scheduling, and planning problems. The submissions have to be in the AMAI format: http://www.springer.com/computer/artificial/journal/10472 and have to be e-mailed to: mvelev@gmail.com If possible, please email by October 10 to express your intent to submit a paper. We look forward to your submission, Miroslav Velev and John Franco Editors of the special issue of AMAI on CFVAI
 
 
 

 
  
Date:27-Apr-2007
Title:Postdoc at Computer Sciences Lab, Australian National University
Hits:1250
Contributed by:
 
  
Date:14-Feb-2007
Title:Paper on Modelling with Logic & Solving with SAT
Hits:1095
Contributed by: David Mitchell
Keywords:Computational logic, SAT tools, Logic, General Interest, SAT-Based, Constraint Programming
 
  
 
One obstacle to wider application of SAT (and related) solvers in applications is the lack of effective modelling languages and tools providing front-ends to the solvers. Our paper "Model Expansion as a Framework for Representing and Solving Search Problems" describes progress to date on a project to address this.

Abstract: We propose a framework for modelling and solving search problems using logic, and describe a project whose goal is to produce practically effective, general purpose tools for representing and solving search problems based on this framework. The mathematical foundation lies in the areas of finite model theory and descriptive complexity, which provide us with many classical results, as well as powerful techniques, not available to many other approaches with similar goals. We describe the mathematical foundations; explain an extension to classical logic with inductive definitions that we consider central; give a summary of complexity and expressiveness properties; describe an approach to implementing solvers based on grounding; present grounding algorithms based on an extension of the relational algebra; describe an implementation of our framework which includes use of inductive definitions, sorts and order; and give experimental results comparing the performance of our implementation with ASP solvers and another solver based on the same framework.

 
 
 

 
  
Date:26-Nov-2006
Title:Special issue of JSAT on CFV
Hits:2111
Contributed by: Miroslav Velev
Keywords:Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, MAC, FC, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, QBF, Dynamic restarts, resolution complexity, message-passing algorithm, Linear Programming, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, Preprocessing, Unit Propagation, symmetry, General Interest, Cellular Automata, Cellection Framework, call for papers, semidefinite programming, conference information, Genetic Algorithm, Boolean functions, SAT-Based, Linear Constraints, SAT Hardware, Lookahead, Generative SAT library, multi-value, Stochastic Satisfiability, Divide-and-Conquer Algorithms, Non-monotonic reasoning, implicativity, stable set of points, stable set of clusters, Satisfiability Modulo Theory, Constraint Programming, genetic programming, SAT/CP, bioinformatics, resolution determinization, SAT-solver, SAT/CP Integration, Hybrid solver, Visualisation, Pseudo-Boolean Solving, Resolution proof
 
  
 
Dear Colleague, We would like to invite you to submit a paper to the special issue of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT) on the topic of application of constraints to formal verification (CFV). The submission deadline is January 10, 2007. Topics include, but are not limited to, the following: - application of constraint solvers to hardware verification; - application of constraint solvers to software verification; - dedicated solvers for formal verification problems; - tuning SAT for formal verification and testing; - challenging formal verification problems. The submissions have to be in the JSAT format: http://www.isa.ewi.tudelft.nl/Jsat/ and have to be e-mailed to: mvelev@gmail.com If possible, please confirm your intent to submit a paper. We look forward to your submission, Miroslav Velev and Joao Marques-Silva Editors of the special issue of JSAT on CFV
 
 
 

 
  
Date:21-Oct-2006
Title:special track on 'applied formal verification' of EuroCAST'07
Hits:1524
Contributed by: Daniel Le Berre
Keywords:DPLL, Local Search, Computational logic, Verification, Alternative approach, QBF, EDA, SAT application, SAT tools, MAXSAT, call for papers, SAT-Based, Satisfiability Modulo Theory, Constraint Programming
 
  
 
special track on 'applied formal verification' of EuroCAST'07 on the
Canarian Islands.

The Workshop concentrates on formal verification engines and to improve
practicability and scalability of formal methods. Topics include, but
not exclusively, the following: Satisfiability (SAT); Satisfiability
Modulo Theories (SMT); Quantified Boolean Formulas (QBF); Constraint
Programming (CP); Equivalence Checking (EC); Model Checking (MC);
Theorem Proving (TP). Case studies and papers in the border line of
verification, including synthesis, compilation and modelling, are also
welcome

Important dates:
  • Extended Abstract, 2 pages, deadline 31. October
  • Decision 1. December
  • Workshop 12.-16. February 2007.
  • Full Papers Post-Conference LNCS Volume, 31. April 2007.
 
 
 

 
  
Date:09-May-2006
Title:Fourth International Workshop on Constraints in Formal Verification (CFV'06)
Hits:1909
Contributed by: Miroslav Velev
Keywords:Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, QBF, Dynamic restarts, resolution complexity, message-passing algorithm, Linear Programming, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, Preprocessing, Unit Propagation, symmetry, General Interest, call for papers, Boolean functions, SAT-Based, Linear Constraints, SAT Hardware
 
  
 
Fourth International Workshop on Constraints in Formal Verification. Affiliated with International Joint Conference on Automated Reasoning 2006 Federated Logic Conference, Seattle, U.S.A., August 22, 2006. The main goals of the Constraints in Formal Verification workshop are to bring together researchers from the CSP/SAT and the formal verification communities, to describe new applications of constraint technology to formal verification, to disseminate new challenging problem instances, and to propose new dedicated algorithms for hard formal verification problems. This workshop will be of interest to researchers from academia and industry, working in constraints or in formal verification and interested in the application of constraints in formal verification. The scope of the workshop includes topics related with the application of constraint technology in formal verification, namely: -application of constraint solvers to hardware verification; -application of constraint solvers to software verification; -dedicated solvers for formal verification problems; -challenging formal verification problems. Submissions can include one of the following: -A workshop paper of up to 15 pages in LNCS format; -A short paper of up to 4 pages, in LNCS format, describing an industrial experience. Important Dates: -Paper submission deadline June 5th; -Notification of acceptance July 5th; -Camera-ready version deadline July 20th; -Workshop Date August 22nd.
 
 
 

 
  
Date:21-Jan-2006
Title:Boolean Functions - Theory, Algorithms, and Applications
Hits:2255
Contributed by: Crama Yves
Keywords:Complexity, Computational logic, Structure of problems, SAT application, Logic, branching heuristics, pseudo boolean optimization, MAXSAT, General Interest, Boolean functions
 
  
 
Together with Peter L. Hammer, we are currently working on a book entitled

BOOLEAN FUNCTIONS - Theory, Algorithms, and Applications

Besides chapters written by Peter and/or myself, the book includes contributions by several leading experts in the field.

The book is devoted to a presentation of the fundamental theory of Boolean functions, with a strong bend toward functions represented in disjunctive normal form. Some of the topics handled in the book are: alternative representations, solution of Boolean equations (SAT), prime implicants, minimization, dualization, decomposition, partially defined functions, etc.

A large section of the book is devoted to the investigation of special classes of Boolean functions: quadratic, Horn, regular, threshold functions, etc.

The book is illustrated by applications arising from various fields, mostly from artificial intelligence, game theory, reliability theory, combinatorics and integer programming.

Drafts of individual sections of the book are available as postscript files on my web page.

 
 
 

 
  
Date:19-Jan-2006
Title:An update has been released of software which compiles a broad class of problems into a SAT formulas.
Hits:2270
Contributed by:
 
  
Date:09-Dec-2005
Title:Mathematics for Satisfiability, Victor Marek notes on Satisfiability
Hits:2286
Contributed by: Daniel Le Berre
Keywords:Deduction Rules, DPLL, DP, Intelligent Backtracking, Data structure, Local Search, Random 3SAT, Complexity, Computational logic, Structure of problems, SAT application, Randomised Algorithms, Learning, CSP, Linear Programming
 
  
 
Almost 350 pages about satisfiability and its applications, from propositional logic to knowledge representation.

Note that the document is still "work in progress" but is quite complete regarding pure SATisfiability.

 
 
 

 
  
Date:10-Nov-2005
Title:CSR-2006 International Computer Science Symposium in Russia
Hits:2320
Contributed by: Daniel Le Berre
Keywords:Deduction Rules, DPLL, DP, Minimal models, Intelligent Backtracking, Local Search, Random 3SAT, Complexity, Computational logic, QBF, SAT application, Equivalency Reasoning, Learning, Model Elimination, SAT tools, Logic, QBF, General Interest, conference information
 
  
 

                                  CSR-2006
             International Computer Science Symposium in Russia

        Sponsored by the U.S. Civilian Research & Development Foundation
    Organized by St.Petersburg Department of Steklov Institute of Mathematics

                   June 8-12, 2006, St.Petersburg, Russia

                            Final Call for Papers

CSR 2006 is the first conference in a series of regular events intended
to reflect the broad scope of international cooperation in computer
science.  CSR 2006 consists of two tracks:

Theory Track:
* algorithms, protocols, and data structures;
* complexity and cryptography;
* formal languages, automata and their applications to computer science;
* computational models and concepts;
* proof theory and applications of logic to computer science.

Applications and Technology Track:
* programming and languages;
* computer architecture and hardware design;
* symbolic computing and numerical applications;
* application software;
* artificial intelligence and robotics.

Program committee:

Theory Track: Sergei Artemov, Paul Beame, Michael Ben-Or, Andrei Bulatov,
  Peter Buergisser, Felipe Cucker, Evgeny Dantsin, Volker Diekert,
  Dima Grigoriev (chair), Yuri Gurevich, Janos Makowsky, Yuri Matiyasevich,
  Peter Bro Miltersen, Grigori Mints, Pavel Pudlak, Prabhakar Raghavan,
  Alexander Razborov, Michael E. Saks, Alexander Shen, Amin Shokrollahi,
  Anatol Slissenko, Mikhail Volkov

Applications and Technology Track: Boris Babayan, Robert Bauer, Matthias Blume,
  Walter Daelemans, Vassil Dimitrov, Sergey Dmitriev, Richard Fateman,
  Dina Goldin, John R. Harrison (chair), John Mashey, Bertrand Meyer,
  Fedor Novikov, Michael Parks, Andreas Reuter, Mary Sheeran,
  Elena Troubitsyna, Miroslav Velev, Sergey Zhukov

The (confirmed) invited speakers include:

* Boaz Barak (Princeton University, USA)
* Gerard Berry (Esterel Technologies, France)
* Bob Colwell (R&E Colwell & Assoc. Inc., USA)
* Byron Cook (Microsoft Research, USA)
* Melvin Fitting (Lehman College and the Graduate Center, CUNY, USA)
* Russell Impagliazzo (University of California at San Diego, USA)
* Michael Kaminski (Technion, Israel)
* Pascal Koiran (Ecole Normale Superieure de Lyon, France)
* Omer Reingold (Weizmann Institute, Israel)

The opening lecture will be given by Stephen A. Cook
(University of Toronto, Canada).

It is planned to publish the proceedings of the symposium in
Springer's LNCS series.

Important dates:
* Paper submission:     December 11, 2005
* Notification:         January 31, 2006
* Symposium:            June 8-12, 2006

There will be limited support for travel expenses of Russian participants.

Further information and contacts:
  Web: http://logic.pdmi.ras.ru/~csr2006/
  Email: csr06chair@logic.pdmi.ras.ru
 
 
 

 
  
Date:30-Jun-2005
Title:Java package for conversion into SAT problem.
Hits:4091
Contributed by:
 
  
Date:08-Oct-2004
Title:Call for Papers for the Journal on Satisfiability, Boolean Modeling and Computation (JSAT)
Hits:2666
Contributed by: Daniel Le Berre
Keywords:Deduction Rules, DPLL, DP, Minimal models, Intelligent Backtracking, Data structure, Local Search, Random 3SAT, Complexity, Randomization, Computational logic, Alternative approach, QBF, Structure of problems, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Satisfiable Problems Generation, SAT tools, branching heuristics, instance database, threshold conjecture, phase transition, binary clause reasoning, Bayesian methods, resolution complexity, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT
 
  
 
Call for Papers for the Journal on Satisfiability, Boolean Modeling and Computation (JSAT)

On behalf of the editorial board it is my pleasure to introduce this new initiative and to invite you to visit

http://www.isa.ewi.tudelft.nl/Jsat/

The intention of JSAT is to be a peer reviewed Journal, publishing high quality original research papers and survey papers which evidently contribute to deeper insight. It is an electronic medium, guaranteeing fast publication.

JSAT contributions are freely on-line accessible.

The scope of JSAT is propositional reasoning, modeling and computation. The Satisfiability discipline is a central focus of JSAT. We welcome all sorts of contributions to this theme but also encourage authors to submit papers on related issues as Computational Logic, Constraint Programming, Quantified Boolean Logic, Pseudo Boolean Methods, zero-one Programming, Integer Programming and Operations Research, whenever the link to Satisfiability is apparent.

To the benefit of the community JSAT also maintains the sites JSAT Addendum and JSAT Links.

Hans van Maaren

 
 
 

 
  
Date:29-Sep-2004
Title:Logic Summer School 2004 The Australian National University
Hits:2036
Contributed by:
 
  
Date:05-Aug-2004
Title:Boolean Functions - Theory, Algorithms, and Applications
Hits:3896
Contributed by: Crama Yves
Keywords:Complexity, Computational logic, Structure of problems, Logic, pseudo boolean optimization, General Interest, Boolean functions
 
  
 
Together with Peter L. Hammer, I am currently working on a book (tentatively) entitled

BOOLEAN FUNCTIONS - Theory, Algorithms, and Applications

Besides chapters written by Peter and/or myself, the book will include contributions by several leading experts in the field.

The book will be devoted to a presentation of the fundamental theory of Boolean functions, with a strong bend toward functions represented in disjunctive normal form. Some of the topics to be handled are: alternative representations, solution of Boolean equations (SAT), prime implicants, minimization, dualization, decomposition, partially defined functions, etc.

A large section of the book will be devoted to the investigation of special classes of Boolean functions: quadratic, Horn, regular, threshold functions, etc.

The book will be illustrated by applications arising from various fields, mostly from artificial intelligence, game theory, reliability theory, combinatorics and integer programming.

Drafts of individual sections of the book are available as postscript files on my web page.

 
 
 

 
  
Date:17-Apr-2004
Title:Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search Henry Kautz & Bart Selman. Invited paper, Ninth International Conference on Principles and Practice of Constraint Programming (CP 2003), Cork, Ireland, 2003.
Hits:2267
Contributed by: Daniel Le Berre
Keywords:DPLL, Minimal models, Intelligent Backtracking, Local Search, Random 3SAT, Complexity, Computational logic, Alternative approach, Structure of problems, SAT application, Learning
 
  
 
This article reviews each of the 10 challenges proposed by the authors in their IJCAI'97 paper and comment them at the light of the recent progress in the area.
 
 
 

 
  
Date:16-May-2003
Title:Vacancy: Assistent professor (permanent) in Logic/Deduction/SAT/OR at Delft University (Netherlands)
Hits:2218
Contributed by: Daniel Le Berre
Keywords:Complexity, Computational logic, Logic
 
  
 
Interested candidates are requested to contact H.vanmaaren@its.tudelft.nl
 
 
 

 
  
Date:08-Feb-2003
Title:Fourth Panhellenic Logic Symposium
Hits:1855
Contributed by: Lefteris Kirousis
Keywords:Computational logic, Logic
 
  
 
ANNOUNCEMENT AND CALL FOR PAPERS

FOURTH PANHELLENIC LOGIC SYMPOSIUM

July 7-10, 2003, Thessaloniki, Greece

The Panhellenic Logic Symposium is a biannual scientific event established in 1997. It is open to researchers from all countries who work on Logic broadly conceived. The language of the Symposium is English. The Fourth Panhellenic Logic Symposium will be hosted at the Conference Center of the International Fair of Thessaloniki, located downtown in close proximity to the University campus. The scientific program of the symposium will consist of hour-long invited talks, tutorials and presentations of accepted papers.

Original papers on all aspects of Logic are solicited. Authors are invited to submit an extended abstract of at most five pages. In addition, the contact author of each paper should send a cover page with his/her addresses (postal and email) and a statement classifying the paper in one of the following areas:

Mathematical Logic,

Set Theory,

Logic in Computer Science,

History of Logic,

Philosophy of Logic,

other Logic related area (specified).

All submitted papers will be reviewed by the scientific committee of the symposium, who will make final decisions on acceptance or rejection. Accepted papers should be presented at the symposium by one of their authors. Each accepted paper will be allocated a thirty-minute period for presentation and questions. Camera-ready extended abstracts not exceeding five pages will be included in a proceedings volume that will be distributed to all participants.

SCIENTIFIC COMMITTEE

S. Cosmadakis (CTI and U. of Patras) C. Dimitracopoulos (U. of Athens) A. Kakas (U. of Cyprus) A. Kechris (Caltech) L. Kirousis (U. of Patras) Chair Ph. Kolaitis (UC Santa Cruz) G. Koletsos (N.T.U. of Athens) E. Kranakis (Carleton U.) M. Mytilinaios (Athens U. of Economics) Th. Pheidas (U. of Crete) A. Sinachopoulos (Archimedia S.A., Athens) P. Spirakis (CTI and U. of Patras) Th. Tzouvaras (U. of Thessaloniki) S. Zachos (N.T.U. of Athens)

ORGANIZING COMMITTEE

C. Dimitracopoulos (U. of Athens) C. Hatzikyriakou (U. of Thessaly) A. Kakas (U. of Cyprus) C. Kalfa (U. of Thessaloniki) A. Sinachopoulos (Archimedia S.A. Athens) Th. Tzouvaras (U. of Thessaloniki) Chair

WEB ADRESS: http://www2.cs.ucy.ac.cy/pls4

INVITED TALKS

D. Bjorner (Technical U. of Denmark)

P. Peppas (U. of Patras)

K. Sagonas (Uppsala U.)

I. Soskov (Sofia U.)

TUTORIALS

Philosophy of Logic: W. Demopoulos (U. of Western Ontario)

Complexity of Logic-Related Problems: E. Koutsoupias (U. of Athens and UCLA)

Logic-Based Information Integration: M. Lenzerini (U. di Roma "La Sapienza") Set Theory: A. Louveau (U. Paris 6)

ADDRESS FOR SUBMISSION

Electronic submissions in PostScript are strongly encouraged

Lefteris Kirousis

Department of Computer Engineering and Informatics University of Patras, University Campus GR-265 04 Patras, GREECE Phone: +30 2610-99 7702 Fax: +30 2610-99 1909 Email: kirousis@ceid.upatras.gr

IMPORTANT DATES

Submission: March 28, 2003

Notification: May 9, 2003

Camera-ready abstracts: May 30, 2003

 
 
 

 
  
Date:06-Sep-2002
Title:Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry, Fadi A. Aloul, Arathi Ramani, Igor L. Markov and Karem A. Sakallah. CSE-TR-463-02, University of Michigan, September 2002
Hits:2149
Contributed by: Igor Markov
Keywords:DPLL, Data structure, Computational logic, Structure of problems, Benchmark, SAT application, Satisfiable Problems Generation
 
  
 
This is a 40-page extension of earlier work reported at SAT 2002 and DAC 2002.
Added are new theorems, proofs, illustrations, algorithms and experimental results.
 
 
 

 
  
Date:23-Aug-2002
Title:Generic ILP versus 0-1 Specialized ILP: An Update,
by F.A.Aloul, A.Ramani, I.L.Markov and K.A.Sakallah

Hits:2082
Contributed by: Igor Markov
Keywords:DPLL, Data structure, Computational logic, Benchmark, SAT tools
 
  
 
Technical Report CSE-TR-461-02 at the Univ. of Michigan.
A related paper will be published in November 2002
in Proc. Intl. Conf. on Computer-Aided Design.

In order to address 0-1 ILP constraints, this work extends recent improvements of backtracking SAT solvers. Our 0-1 ILP solver can also optimize a function with 0-1 variables subject to 0-1 ILP constraints. Empirical validation is performed by comparing with other 0-1 ILP solvers, including CPLEX.

 
 
 

 
  
Date:14-Jul-2002
Title:A polynomial time SAT algorithm
Hits:7326
Contributed by: Anonymous
Keywords:Complexity, Computational logic, Alternative approach
 
  
 
An algorithm of two parts is presented that determines existence of and instance of an assignment satisfying of instances of SAT. The algorithm employs an unconventional approach premised on set theory, which does not use search or resolution, to partition the set of all assignments into non-satisfying and satisfying assignments. The algorithm, correctness, and time and space complexity proofs are given.
 
 
 

 
  
Date:13-Mar-2002
Title:SAT papers are invited to the Journal of Universal Computer Science (J.UCS).
Hits:2637
Contributed by: Miroslav Velev
Keywords:Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, #P, Data structure, Quasigroups, Local Search, Repository, BDD, Random 3SAT, Stalmark, Complexity, Randomization, Computational logic, MAC, FC, Verification, Alternative approach, QBF, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, Satisfiable Problems Generation, SAT tools, Distributed Computing, CSP, Logic
 
  
 
 
 
 
 

 
  
Date:29-Jun-2001
Title:Seventh International Symposium on Artificial Intelligence and Mathematics
Hits:2232
Contributed by:
 
  
Date:20-Jun-2001
Title:Compiling problem specifications into SAT. by M. Cadoli, A. Schaerf. Proc. of ESOP'01, April 2001. Published in volume 2028 of Springer LNCS series © Springer-Verlag.
Hits:2027
Contributed by:
 
  
Date:18-Apr-2001
Title:8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Hits:2011
Contributed by:
 
  
Date:20-Sep-2000
Title:2nd Australasian Workshop on Computational Logic
Hits:1797
Contributed by:

 

© 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.