 |
13 elements available |  | |  | | | | | Date: | 17-Jan-2013 | | Title: | Internship Position at IBM Research, AI for Optimization group
| | Hits: | 247 | | Contributed by: | Ashish Sabharwal | | Keywords: | Local Search, SAT application, Learning, SAT tools, Distributed Computing, CSP, Linear Programming, pseudo boolean optimization, Genetic Algorithm, New research position, Satisfiability Modulo Theory, Constraint Programming, Job, SAT/CP Integration, null, null, null, null, null, null, null |
| | | |  |  | |
| | A summer internship position is available for 2013 in the "AI for Optimization" group within the Business Analytics and Mathematical Sciences department at IBM Watson Research Center, Yorktown Heights, New York. The internship will last for about 3 months and will be scheduled between March and October, 2013.
Candidates should be exceptional Masters or PhD students in Computer Science and related areas, and not have already received their PhD by the internship start date. The successful candidate is expected to have strong interest and some experience in one or more of the following:
- Developing Novel Technologies based on AI and OR to advance the state of the art in combinatorial optimization (e.g., Heuristic Search, Mixed Integer Programming (MIP), Linear Programming (LP), Satisfiability (SAT))
- Robust Parallelization of search-based algorithms (e.g., using parallel Branch&Bound; information exchange) exploiting novel computing architectures such as BlueGene, multi-core end-user machines, large compute clusters, and the Cloud
- Advancing Simulation-Based Optimization approaches to solve real-world problems and/or to improve optimization methods themselves by, e.g., employing techniques from Machine Learning, Local Search, and Genetic Algorithms for automated algorithm selection and parameter tuning
- Applications of Optimization to Analytics, Production Modeling, Sustainability, Systems, and Databases
Interested candidates should send their CV as well as names and contact information of at least two references to all of the following:
Ashish Sabharwal [ashish.sabharwal@us.ibm.com]
Horst Samulowitz [samulowitz@us.ibm.com]
Meinolf Sellmann [meinolf@us.ibm.com] |
| |  | |  |
| | |
| | | [ We apologize if you receive multiple copies of this call. ]
-------------------------------------------------------------------------
1ST CALL FOR WORKSHOPS, COMPETITIONS, AND TUTORIALS
Sixteenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2013 ---
Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/
-------------------------------------------------------------------------
THIS DOES NOT CONTAIN A CALL FOR PAPERS. THAT CALL WILL APPEAR SOON.
-------------------------------------------------------------------------
PROPOSAL SUBMISSION DEADLINE: November 2, 2012
Proposals should be submitted by email to sat2013@easychair.org, either in
ASCII text or as an attachment in PDF form, and should include
in sufficient detail the information outlined below.
Proposals with incomplete information may be submitted, in case the deadline
is a bit early. Please indicate in your proposal a plan and/or schedule
for getting the remaining information.
------------------------------------------------------------------------- |
| | | | |
| | |
| | | | | | | | Date: | 05-Sep-2012 | | Title: | ASPCOMP 2013: 4th OPEN Answer Set Programming Competition: Call for Benchmark Problems (EXTENDED DEADLINE)
| | Hits: | 328 | | Contributed by: | Anonymous | | Keywords: | Deduction Rules, DPLL, Minimal models, #P, Computational logic, QBF, Structure of problems, Benchmark, SAT application, Randomised Problem Generation, SAT tools, CSP, Logic, QBF, programming language, General Interest, call for papers, conference information, Non-monotonic reasoning, Satisfiability Modulo Theory, Constraint Programming, SAT/CP, Answer Set Programming, null, null, null, null, null |
| | | | | | |
| |
........................................................................
4th OPEN Answer Set Programming Competition 2013
Call for Benchmark Problems
University of Calabria - Vienna University of Technology
Fall/Winter 2012/2013
http://aspcomp2013.mat.unical.it/
........................................................................
The 4th Open Answer Set Programming Competition is open to ASP systems
and *any other system* based on a declarative specification paradigm.
The event is currently finalizing its Call for Benchmarks stage.
== Call for Benchmark Problems ==
Participants will compete on a selected collection of declarative
specifications of benchmark problems, taken from a variety of domains as
well as real world applications, and instances thereof.
These include, but are not limited to:
- Deductive database tasks on large data-sets
- Sequential and Temporal Planning
- Classic and Applicative graph problems
- Puzzles and Combinatorics
- Scheduling, Timetabling, and other resource allocation problems
- Combinatorial Optimization Problems
- Ontology reasoning
- Automated Theorem Proving and Model Checking
- Reasoning tasks over large propositional instances
- Constraint Programming problems
- Other AI problems
We encourage to provide help by proposing and/or devising new challenging
benchmark problems.
The submission of problems arising from applications of practical impact
are strongly encouraged; problems used in the former ASP Competitions,
or variants thereof, can be re-submitted.
Benchmark authors are expected to produce a problem specification and an
instance set (or a generator thereof). The detailed benchmark problems
submission procedure is available at:
http://www.mat.unical.it/aspcomp2013/BenchmarkSubmission.
=== About the ASP Competition Series ===
Answer Set Programming is a well-established paradigm of declarative
programming with close relationship to other declarative modeling
paradigms and languages, such as SAT Modulo Theories, Constraint
Handling Rules, FO(.), PDDL, CASC, and many others.
Since the first informal editions (Dagstuhl 2002 and 2005), ASP systems
compare themselves in the nowadays customary ASP Competition: the 4th
ASP Competition will be run jointly at the University of Calabria
(Italy) and the Vienna University of Technology (Austria), in the first
half of 2013. The event is the sequel to the ASP Competition series,
held at the University of Potsdam (Germany) in 2006-2007, at the
University of Leuven (Belgium) in 2009, and at University of Calabria
(Italy) in 2011. The current competition takes place in cooperation with
the 13th International Conference on Logic Programming and Nonmonotonic
Reasoning (LPNMR 2013), where the results will be announced.
The ASP competition is held as an open tournament. The "Model & Solve"
competition track fosters the spirit of integration among communities,
and is thus open to all types of solvers: ASP systems, SAT solvers, SMT
solvers, CP systems, FOL theorem provers, Description Logics reasoners,
planning reasoners, or any other. The "System" competition track is
instead set up on a fixed language based on the answer set semantics.
== Important Dates ==
* Problem selection stage
- Problem submission deadline: Sep 20th, 2012 (*EXTENDED*)
* Competition stage
- "Model & Solve" submission deadline: Mar 1st, 2013
- "System" submission deadline: Mar 1st, 2013
* Sep 15-19th, 2013
- Announcement of results and awards at LPNMR 2013 - Corunna, Spain
== Further Information ==
For further information please visit the competition web site:
http://aspcomp2013.mat.unical.it/
or contact us by email: aspcomp2013@kr.tuwien.ac.at.
|
| | | | |
| | |
| |
---------------------------------------------------------------------------
[[[ We apologize if you receive multiple copies of this message ]]]
---------------------------------------------------------------------------
Job Description:
=================
The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for the verification of
circuit designs in particular the use of Satisfiability Modulo Theories
(SMT), however researcher with background on other verification techniques
are also encouraged to apply.
Candidate Profile:
=================
World class researcher in EE/CS/Math (particularly formal theory),
familiar with predicate logic, temporal logic (e.g., CTL, LTL), model
checking, familiar with complexity of algorithms, very strong in
algorithm development -- including design and implementation of large programs,
very strong in mathematical considerations in the development of CAD tools/EDA
and familiarity with design practice. Intimate knowledge of solvers such as BDD,
SAT, ATPG, SMT and symbolic simulation algorithms. Capability of working with
prospective customers. Experience in a Semiconductor company is helpful but not
absolutely essential.
Job Requirements:
=================
BS in EE/CS/Math. with 9+ years of relevant experience, MS with 7+ years of
relevant experience, or related Ph.D.
It is essential that the individual has strong desires to learn and
explore new technologies and are able to demonstrate good analysis and problem
solving skills. Prior knowledge and experience of CAD tool/EDA development are
a big plus.
Job site:
=========
The researcher will be part of Atrenta's EU based advanced research center
and can work from any EU country.
The company will not sponsor immigration visa.
Contact Person
==============
Fahim@atrenta.com
|
| | | | |
| | |
| | | | | | | | Date: | 03-Feb-2012 | | Title: | SMT Workshop 2012
| | Hits: | 228 | | Contributed by: | Roberto Bruttomesso | | Keywords: | Satisfiability Modulo Theory, SAT/CP Integration, null, null, null, null, null, null, null, null, null, null |
| | | | | | |
| |
======================================================================
SMT Workshop 2012
10th International Workshop on Satisfiability Modulo Theories
Affiliated with IJCAR’2012, Manchester, UK
June 30th - July 1st, 2012
Collocated with The Alan Turing Centenary Conference
http://smt2012.loria.fr
---CALL FOR PAPERS---
======================================================================
Background
----------
Determining the satisfiability of first-order formulas modulo
background theories, known as the Satisfiability Modulo Theories (SMT)
problem, has proved to be an enabling technology for verification,
synthesis, test generation, compiler optimization, scheduling, and
other areas. The success of SMT techniques depends on the development
of both domain-specific decision procedures for each background theory
(e.g., linear arithmetic, the theory of arrays, or the theory of
bit-vectors) and combination methods that allow one to obtain more
versatile SMT tools, usually leveraging Boolean satisfiability (SAT)
solvers. These ingredients together make SMT techniques well-suited
for use in larger automated reasoning and verification efforts.
Aims and Scope
--------------
The aim of the workshop is to bring together researchers and users of
SMT tools and techniques. Relevant topics include but are not limited to:
* Decision procedures and theories of interest
* Combinations of decision procedures
* Novel implementation techniques
* Benchmarks and evaluation methodologies
* Applications and case studies
* Theoretical results
Papers on pragmatic aspects of implementing and using SMT tools, as well
as novel applications of SMT, are especially encouraged.
Important dates
---------------
* Submission deadline - April 16th, 2012
* Notification - May 7th, 2012
* Camera ready versions due - May 28th, 2012
* Workshop - June 30th and July 1st, 2012
Paper submission and Proceedings
--------------------------------
Three categories of submissions are invited:
* Extended abstracts: given the informal style of the workshop, we
strongly encourage the submission of preliminary reports of work in
progress. They may range in length from very short (a couple of
pages) to the full 10 pages and they will be judged based on the
expected level of interest for the SMT community. They will be
included in the informal proceedings.
* Original papers: contain original research (simultaneous submissions
are not allowed) and sufficient detail to assess the merits and
relevance of the submission. For papers reporting experimental
results, authors are strongly encouraged to make their data
available.
* Presentation-only papers: describe work recently published or
submitted and will not be included in the proceedings. We see this
as a way to provide additional access to important developments that
SMT Workshop attendees may be unaware of.
Papers in all three categories will be peer-reviewed. Papers should
not exceed 10 pages (Postscript or PDF) and should be in
standard-conforming Postscript or PDF. Technical details may be
included in an appendix to be read at the reviewers' discretion.
Final versions should be prepared in LaTeX using the easychair.cls
class file.
To submit a paper, go to the EasyChair SMT page
http://www.easychair.org/conferences/?conf=smt2012 and follow the
instructions there.
|
| | | | |
| | |
| | Job Description:
=================
The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for the verification of circuit designs in particular the use of Satisfiability Modulo Theories (SMT), however researcher with background on other verification techniques are also encouraged to apply.
Candidate Profile:
=================
World class researcher in EE/CS/Math (particularly formal theory), familiar with predicate logic, temporal logic (e.g., CTL, LTL), model checking, familiar with complexity of algorithms, very strong in algorithm development -- including design and implementation of large programs, very strong in mathematical considerations in the development of CAD tools/EDA and familiarity with design practice.
Intimate knowledge of solvers such as BDD, SAT, ATPG, SMT and symbolic simulation algorithms.
Capability of working with prospective customers. Experience in a Semiconductor company is helpful but not absolutely essential.
Job Requirements:
=================
BS in EE/CS/Math. with 9+ years of relevant experience, MS with 7+ years of relevant experience, or related Ph.D.
It is essential that the individual has strong desires to learn and explore new technologies and are able to demonstrate good analysis and problem solving skills. Prior knowledge and experience of CAD tool/EDA development are a big plus.
Job site:
=========
The researcher will be part of Atrenta's EU based advanced research center and can work from any EU country.
The company will not sponsor immigration visa.
Contact Person
==============
Fahim@atrenta.com
|
| | | | |
| | |
| |
The SAT/SMT Summer School 2012 (2nd edition) aims at providing graduate
students and researchers from universities and industry with a
comprehensive overview of the research in SAT, SMT, and their
application. The lectures cover the foundational and practical aspects
of SAT and SMT solvers, as well as their application to verification,
planning, scheduling, and optimization problems.
This second edition follows the Summer School of 2011 organized by Vijay
Ganesh at MIT, and is co-located with the SAT 2012 conference. The
school will take place in Trento, Italy, from June 12th to June 15th
2012.
The program will feature four lectures per day, with the first two days
dedicated to SAT and SMT foundations, and the last two to applications
on various domains.
List of speakers:
- Armin Biere (Johannes Kepler University, Linz, Austria)
- Leonardo de Moura (Microsoft Research Redmond, USA)
- Bruno Dutertre (SRI International, USA)
- Martin Fränzle (Carl von Ossietzky Universität Oldenburg, Germany)
- John Franco (University of Cincinnati, USA)
- Silvio Ghilardi (Università di Milano, Italy)
- Patrice Godefroid (Microsoft Research Redmond, USA)
- Holger Hoos (University of British Columbia, Vancouver, Canada)
- Tomi Janhunen (Aalto University, Finland)
- Pete Manolios (Northeastern University, USA)
- Joao Marques-Silva (University College Dublin, Ireland)
- Ken McMillan (Microsoft Research Redmond, USA)
- Jussi Rintanen (Austrialian National University, Australia)
- Fabio Somenzi (University of Colorado, Boulder, USA)
- Gunnar Stålmarck (Prover Technology and Gain Sweden AB, Sweden)
- Cesare Tinelli (University of Iowa, USA)
A more detailed program is available at the school website
(http://satsmtschool2012.fbk.eu).
It is expected that we will be able to provide a limited number of
grants for students that will attend the school. More details about the
procedure for applying and the registration deadlines will appear on the
school website as soon as possible. Interested students are however
encouraged to contact us at any moment.
The school organizers,
Alberto Griggio <griggio@fbk.eu> and
Stefano Tonetta <tonettas@fbk.eu> |
| | | | |
| | |
| |
======================================================================
7th International Satisfiability Modulo Theories Competition
(SMT-COMP'11)
July 14 - 20, 2011
Snowbird, Utah
CALL FOR BENCHMARKS
CALL FOR ENTRANTS
======================================================================
|
| | | | |
| | |
| | | | | | | | Date: | 24-Jan-2011 | | Title: | Aalto University: Three tenure track positions in information and computer science
| | Hits: | 701 | | Contributed by: | Ilkka Niemela | | Keywords: | Complexity, SAT application, Logic, Linear Programming, Non-monotonic reasoning, Satisfiability Modulo Theory, Constraint Programming, null, null, null, null |
| | | | | | |
| | | Aalto University School of Science (Helsinki, Finland) invites applications for three tenured of tenure track positions in the Department of Information and Computer Science (http://ics.tkk.fi/en/) open to outstanding individuals who hold a doctorate and have excellent potential for a successful scientific career.
Closing Date for Applications: 2011-02-04
For more details, see http://dept.ics.tkk.fi/calls/tenuretrack2011/ |
| | | | |
| | |
| |
There is an opening for one doctoral student in Automated Software Analysis research group (http://asa.iti.kit.edu/) in the department of Informatics at Karlsruhe Institute of Technology, Germany. The project involves using SMT solvers in a novel way to find bugs in object-oriented programs, and will be supervised by Juniorprof. Dr. Mana Taghdiri.
The ideal candidate should hold an MS or equivalent degree in computer science, or mathematics, and should have strong communication skills (both speaking and writing) in English. Solid theoretical background in formal methods and logic, as well as programming experience in Java and/or C++ is required. Suitable candidates must posses a strong willingness for research exploration, independence, self-learning, creativity, and teamwork.
The selected candidate is expected to start as soon as possible, and will be funded based on the salary grade TV-L, E13.
The application material (resume, transcripts, and names of potential references) should be emailed to mana.taghdiri@kit.edu
|
| | | | |
| | |
| |
The Complex and Adaptive Systems Laboratory is opening three post-doctoral
positions in the area of Boolean-based constraint solving and optimization.
The post-doctoral researchers will be involved in developing new decision
and optimization procedures for Satisfiability Modulo Theories (SMT) and
Boolean Satisfiability (SAT).
Applicants should have a undergraduate degree in Computer Science or
related discipline. Experience with tool development is desirable. The
post-doctoral researcher appointments will be for either 1 or 3 years.
The salary for post-doctoral researchers varies between 37750 EUR and
46255 EUR, depending on experience.
More information is available at http://www.csi.ucd.ie/staff/jpms/vacancies/
and at http://www.ucd.ie/hr/jobvacancies/. Informal enquiries should be
directed to Prof. Joao Marques-Silva (http://www.csi.ucd.ie/staff/jpms/).
|
| | | | |
| | |
| | | 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/ |
| | | | |
| | |
| | | Abstract Most, if not all, state-of-the-art complete SAT solvers are complex variations of the DPLL procedure described in the early 1960’s. Published descriptions of these modern algorithms and related data structures are given either as high-level state transition systems or, informally, as (pseudo) programming language code. The former, although often accompanied with (informal) correctness proofs, are usually very abstract and do not specify many details crucial for efficient implementation. The latter usually do not involve any correctness argument and the given code is often hard to understand and modify. This paper aims to bridge this gap by presenting SAT solving algorithms that are formally proved correct and also contain information required for efficient implementation. We use a tutorial, top-down, approach and develop a SAT solver, starting from a simple design that is subsequently extended, step-by-step, with a requisite series of features. The heuristic parts of the solver are abstracted away, since they usually do not affect solver correctness (although they are very important for efficiency). All algorithms are given in pseudo-code and are accompanied with correctness conditions, given in Hoare logic style. The correctness proofs are formalized within the Isabelle theorem proving system and are available in the extended version of this paper. The given pseudo-code served as a basis for our SAT solver argo-sat. |
| | | | |
| | |
© 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.
|
|
|
