Deadline Countdown

Heads up on SAT research

SAT related books

Other SAT related sites

Date: 18-May-2010 Title: SofT'10 - 10th Workshop on Preferences and Soft Constraints Hits: 151 Contributed by: Joao Marques-Silva Keywords: MAXSAT, call for papers, SoftSAT, null         10th Workshop on Preferences and Soft Constraints, SofT'10 Held in conjunction with the 16th International Conference on Principles and Practice of Constraint Programming, CP'10 Technical Description --------------------- Preferences are ubiquitous in real life: most problems are over-constrained and would not be solvable if we insist that all their requirements are strictly met. Moreover, many problems are more naturally described via preference rather than hard statements. Soft constraints are the way the constraint community has extended its classical framework to deal with the concept of preferences. This workshop will bring together researchers interested in all aspects of soft constraints and cost function processing, such as: - theoretical frameworks - problem modeling - solving algorithms - languages - preference aggregation and elicitation - multi-objective or qualitative optimization - combining/integrating different frameworks and algorithms - comparative studies - real-life applications The workshop is an opportunity to share knowledge between people working in algorithms and solvers for formalisms, including Weighted Max-SAT, Soft CSP, Bayesian Networks, Random Markov Field, Factor Graphs, Pseudo Boolean Optimization, SAT Modulo Theories, and related formalisms. Workshop Format --------------- This workshop is intended to build on the experience and success of the CP'99 to CP'06 workshops on the same subject and the recent meeting on cost function processing (25 attendees during two days). Its aim is to provide a forum where researchers currently working in this area can discuss their most recent ideas and developments and think together about the most promising new directions. Therefore, we encourage the presentation of work in progress or on specialized aspects of preferences, soft constraints, and more generally, cost function processing. Papers that bridge the gap between theory and practice are especially welcome. Paper Submission ---------------- Paper submissions should contain original material and must not exceed 15 pages. Submissions should use the Springer LNCS style. All appendices, tables, figures and the bibliography must fit into the page limit. Submissions deviating from these requirements may be rejected without review. Paper submission and reviewing will be done via EasyChair. The paper submission page is: http://www.easychair.org/conferences/?conf=soft10. Important dates ---------------- Paper Submission June 18 Notification July 23 Final Versions August 8 Workshop Date September 6 Workshop Organizers -------------------- Simon de Givry, INRA, Toulouse, France Felip Manya, CSIC, Barcelona, Spain Joao Marques-Silva, University College Dublin, Ireland Program Committee --------------------- Fahiem Bacchus, University of Toronto, Canada Hachemi Bennaceur, CRIL, France Stefano Bistarelli, University of Perugia, Italy Jimmy Lee, Chinese Univ. of Hong Kong, China Chu-Min Li, Université de Picardie, France Ines Lynce, Technical Univ. of Lisbon, Portugal Pedro Meseguer, CSIC, Spain Thierry Petit, LINA-CNRS, France Jordi Planes, Universitat de Lleida, Spain Emma Rollon, Technical Univ. of Catalonia, Spain Thomas Schiex, INRA, France Francesca Rossi, University of Padova, Italy Brent Venable, University of Padova, Italy Gerard Verfaillie, ONERA, France Tomas Werner, Czech Tech. Univ., Czech Republic Nic Wilson, 4C, Ireland

Date: 09-Mar-2010 Title: Pseudo-Boolean Competition 2010 Hits: 231 Contributed by: Olivier ROUSSEL Keywords: pseudo boolean optimization, MAXSAT, Linear Constraints, SAT-Solver Competition, Pseudo-Boolean Solving, null         The fifth competition of pseudo-Boolean solvers is organized as a special event of the SAT 2010 conference. Like the previous evaluations and competitions, the goal is to assess the state of the art in the field of pseudo-Boolean solvers. The 2010 competition is very similar to the 2009 edition, with 2 exceptions: non linear objective functions are allowed a special track and a new format are dedicated to maximum satisfiability and weighted max-satisfiability on PB constraints We encourage you to submit solvers and/or benchmarks to the competition by May 9. All details are available on the competition web site: http://www.cril.univ-artois.fr/PB10/

Date: 19-Feb-2010 Title: Pragmatics of SAT, a workshop of the SAT conference within the Federated Logic Conference (FLoC) - July 10, 2010 - Edinburgh, Scotland, UK Hits: 276 Contributed by: Daniel Le Berre Keywords: Structure of problems, Benchmark, SAT application, SAT tools, branching heuristics, Dynamic restarts, programming language, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, distributed parallel dynamic learning, symmetry, General Interest, Boolean functions, SAT-Based, Linear Constraints, Stochastic Satisfiability, SAT-Solver Competition, Satisfiability Modulo Theory, bioinformatics, SAT-solver, Hybrid solver, Pseudo-Boolean Solving, null, null, null, null, null         Pragmatics of SAT a workshop of the SAT conference within the Federated Logic Conference (FLoC) 2010 July 10, 2010 - Edinburgh, Scotland, UK The aim of the pragmatics of SAT workshop is to allow researchers concerned with the design of efficient SAT solvers or SAT encodings to meet and discuss about their latest results. The workshop is also the place for users of SAT technology to present their applications. This workshop follows the spirit of Pragmatics of Decision Procedures in Automated Reasoning organized at FLoC 2006. Topics Main areas of interest include, but are not restricted to: * techniques for debugging or certifying solvers * visualisation of benchmarks structure * monitoring solver behaviour * evaluation of solvers * efficient data structures * domain specific encodings * taking into account multi-core technology * domain specific heuristics * new application of sat technology * system/library description Submission There are two possible type of submissions for the workshop. The papers are supposed to be submitted electronically through EasyChair as a PDF file using the LNCS style (the same as the SAT conference). http://www.easychair.org/conferences/?conf=pos10 * Regular papers (up to 14 pages). Accepted papers will be published in the CEUR-WS electronic proceedings. * System descriptions (up to 6 pages). Accepted papers will be published in the JSAT journal, in the new system description category. The final format of the paper will be different: system descriptions will be published as a 4 page JSAT style while regular paper will use a specific workshop style. Authors should provide enough information and/or data for reviewers to confirm any performance claims. This includes links to a runnable system, access to benchmarks, reference to a public performance results, etc. The system description category especially targets the authors of the systems that enter the SAT 2010 conference competitive events (SAT Race 2010, PB 2010, MAXSAT 2010, QBFEVAL 2010, ...). The aim of this workshop is to push forward peer-reviewed published system descriptions as a means to spread technical information regarding the design of solvers. System descriptions are expected to describe briefly but precisely the main features of the system, in a specific version. Regular papers provide more space to describe in detail a full system or application, provide experimental results, etc. Important dates * Submission deadline: March 26, 2010. * Authors notification: April 23, 2010. * Final version due: May 15, 2010. * The workshop will take place on July 10th, 2010. Tutorial by Youssef Hamadi: From Parallel SAT to Distributed SAT This tutorial will present an overview of parallelism in SAT. It will start with a presentation of classical divide and conquer techniques, discuss their ancient origin and compare them to more recent portfolio-based algorithms. It will then present the impact of clause-sharing on their performances and discuss various strategies used to control the communication overhead. A particular technique used to control the classical diversification/intensification tradeoff will also be presented. Finally, perspectives will be given which will relate the current parallel SAT technologies to the expected evolution of computational platforms, leading to distributed SAT solving scenarios. Programme Committee * Josep Argelich * Armin Biere * Youssef Hamadi * Daniel Le Berre * Olivier Roussel * Carsten Sinz * Armando Tacchella * Allen Van Gelder

Date: 06-Jul-2009 Title: MAXSAT 09 competition results available Hits: 407 Contributed by: Daniel Le Berre Keywords: MAXSAT         The results of the fourth MAXSAT competition are now available. Detailed information about the solvers and benchmarks will be available soon.

Date: 27-May-2009 Title: SAT4J 2.1 released! Hits: 419 Contributed by: Daniel Le Berre Keywords: SAT tools, pseudo boolean optimization, MAXSAT         The new release focuses mainly in simplifying the integration and the use of the solvers in Java programs. The release includes also improved pseudo boolean and maxsat solvers. SAT4J 2.1 core and pseudo packages will ship with Eclipse 3.5 next month.

Date: 26-May-2009 Title: J. Argelich, I. Lynce and J.P. Marques Silva, On Solving Boolean Multilevel Optimization Problems, IJCAI'09, July 2009. Hits: 330 Contributed by: Daniel Le Berre Keywords: SAT application, pseudo boolean optimization, MAXSAT         Abstract: Many combinatorial optimization problems entail a number of hierarchically dependent optimization problems. An often used solution is to associate a suitably large cost with each individual optimization problem, such that the solution of the resulting aggregated optimization problem solves the original set of optimization problems. This paper starts by studying the package upgradeability problem in software distributions. Straightforward solutions based on Maximum Satisfiability (MaxSAT) and pseudo-Boolean (PB) optimization are shown to be ineffective, and unlikely to scale for large problem instances. Afterwards, the package upgradeability problem is related to multilevel optimization. The paper then develops new algorithms for Boolean Multilevel Optimization (BMO) and highlights a number of potential applications. The experimental results indicate that algorithms for BMO allow solving optimization problems that existing MaxSAT and PB solvers would otherwise be unable to solve.

Date: 16-Apr-2009 Title: Modeling and Reasoning with Bayesian Networks by Adnan Darwiche, Cambridge University Press Hits: 546 Contributed by: Daniel Le Berre Keywords: SAT application, Bayesian methods, MAXSAT, null         The book provides an advanced introduction to Bayesian networks, written mostly from a knowledge representation and reasoning perspective. It emphasizes semantics, and discusses SAT-based techniques for Bayesian network inference, including SAT encodings, maxsat, model counting and knowledge compilation. More details on the book -- including a table of contents and a full search through its chapters -- can be found on Amazon.

Date: 01-Feb-2009 Title: Handbook of Satisfiability, Volume 185 Frontiers in Artificial Intelligence and Applications, Edited by: A. Biere, M. Heule, H. Van Maaren and T. Walsh, February 2009, 980 pp., hardcover ISBN: 978-1-58603-929-5 Hits: 601 Contributed by: Daniel Le Berre Keywords: BMC, DPLL, Intelligent Backtracking, Data structure, Local Search, Random 3SAT, Complexity, Structure of problems, Benchmark, SAT application, Instance simplification, Learning, SAT tools, branching heuristics, phase transition, binary clause reasoning, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, Preprocessing, symmetry, General Interest, SAT-Based, Lookahead, SAT-solver         “Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas. Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field.” Edmund Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award)

Date: 17-Jul-2008 Title: Post-Doctoral Position Hits: 726 Contributed by:       Date: 26-Jun-2008 Title: SofT'08 - 9th Workshop on Preferences and Soft Constraints (Deadline extended) Hits: 807 Contributed by:       Date: 08-Jun-2008 Title: SofT'08 - 9th Workshop on Preferences and Soft Constraints (2nd Call for Papers) Hits: 789 Contributed by:       Date: 29-Apr-2008 Title: SofT'08 - 9th Workshop on Preferences and Soft Constraints Hits: 956 Contributed by:       Date: 04-Apr-2008 Title: Symmetry Breaking for Maximum Satisfiability, Joao Marques-Silva, Ines Lynce, Vasco Manquinho, arXiv:0804.0599v1 Hits: 542 Contributed by: Daniel Le Berre Keywords: MAXSAT, symmetry         Symmetries are intrinsic to many combinatorial problems including Boolean Satisfiability (SAT) and Constraint Programming (CP). In SAT, the identification of symmetry breaking predicates (SBPs) is a well-known, often effective, technique for solving hard problems. The identification of SBPs in SAT has been the subject of significant improvements in recent years, resulting in more compact SBPs and more effective algorithms. The identification of SBPs has also been applied to pseudo-Boolean (PB) constraints, showing that symmetry breaking can also be an effective technique for PB constraints. This paper extends further the application of SBPs, and shows that SBPs can be identified and used in Maximum Satisfiability (MaxSAT), as well as in its most well-known variants, including partial MaxSAT, weighted MaxSAT and weighted partial MaxSAT. As with SAT and PB, symmetry breaking predicates for MaxSAT and variants are shown to be effective for a representative number of problem domains, allowing solving problem instances that current state of the art MaxSAT solvers could not otherwise solve.             Date: 27-Feb-2008 Title: MaxSAT Evaluation 2008 Hits: 707 Contributed by: Jordi Planes Keywords: MAXSAT         Dear all, We are pleased to announce the call for benchmarks and solvers for the MaxSAT Evaluation 2008, http://www.maxsat.udl.cat/. This year, there will be several changes to the MaxSAT evaluation: 1. You are asked to register on the MaxSAT evaluation web site before submitting a solver or benchmarks. A code will then be provided, that can be used for future submissions (as many as you like, until the deadline). 2. The file formats of the previous evaluation will be accepted. However, benchmarks may be provided in new formats, aiming smaller file sizes. The new formats which will soon be available at the MaxSAT evaluation website. Benchmarks can be submitted in any format, and they will be translated as required. All solvers should be able to read last year's formats. 3. For registering benchmarks, and in additional to the category (maxsat, partial maxsat, weighted maxsat, and weighted partial maxsat), you need to select the benchmark class. A benchmark can belong to any of the three following classes: a. Random, if it is artificially created without any structure; b. Crafted, if it is artificially created but has some structure; c. Industrial, if it is not artificially created. The schedule for the MaxSAT evaluation will be the following: A. The deadline for the first submission will be in March 9th. B. Afterwards, there will be a week for fixing solver bugs, using instances that will be provided for this purpose. C. March 16th will be the final submission deadline for corrected solvers. D. Afterwards the MaxSAT evaluation will take place. Feel free to distribute this e-mail to anyone interested on submitting benchmarks or solvers to the MaxSAT evaluation. --- MaxSAT Evaluation organizers             Date: 09-Jan-2008 Title: MaxSAT solver msuncore Hits: 1035 Contributed by:       Date: 03-Jan-2008 Title: Using Online Algorithms to Solve NP-Hard Problems More Efficiently in Practice, Matthew Streeter, CMU-CS-07-172, December 2007 Hits: 903 Contributed by: Daniel Le Berre Keywords: Structure of problems, SAT application, Dynamic restarts, pseudo boolean optimization, MAXSAT, Pseudo-Boolean Solving, null         School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 Thesis Committee: Stephen F. Smith, chair Avrim Blum Tuomas Sandholm Carla P. Gomes, Cornell University John N. Hooker, CMU Tepper School of Business Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy.             Date: 15-Nov-2007 Title: Post-Doctoral Position Hits: 1235 Contributed by:       Date: 26-Oct-2007 Title: Maxsat solver MaxSatz Hits: 1164 Contributed by: chuMin Li Keywords: MAXSAT         A branch and bound solver for Max-SAT that incorporates into a Max-SAT solver some of the technology developed for Satz (see below). At each node of the proof tree it transforms the formula into an equivalent formula that preserves the number of unsatisfied clauses by applying some efficient refinements of unit resolution that the authors have defined for Max-SAT (e.g., it replaces $x, y, eg x vee eg y$ with $Box, x vee y$, it replaces $x, eg x vee y, eg x vee z, eg y vee eg z$ with $Box, eg x vee y vee z, x vee eg y vee eg z$). MaxSatz implements a lower bound computation method that consists of incrementing the lower bound by one for every disjoint inconsistent subset that can be detected by unit propagation. Moreover, the lower bound computation method is enhanced with failed literal detection. The variable selection heuristics takes into account the number of positive and negative occurrences in binary and ternary clauses. Maxsatz and its variants are the best performing solvers in the unweighted maxsat category in the 2006 maxsat solvers evaluation and the 2007 maxsat solvers evaluation. References: Chu Min LI, Felip Manya, Jordi Planes, "New Inference Rules for Max-SAT", in Journal of Artificial Intelligence Research, October 2007, Volume 30, pages 321-359 Chu Min LI, Felip Manya, Jordi Planes, "Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT". In Proceedings of the 21st National Conference on Artificial Intel ligence (AAAI-06), Boston, USA, pp. 86–91. AAAI Press.             Date: 26-Oct-2007 Title: New Inference Rules for Max-SAT Hits: 788 Contributed by: chuMin Li Keywords: MAXSAT         Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.             Date: 30-Aug-2007 Title: SAT4J 1.7 released Hits: 1044 Contributed by: Daniel Le Berre Keywords: SAT tools, pseudo boolean optimization, MAXSAT, SAT-Based, SAT-solver         Among the new features: * New SAT solver presented to the SAT Race 2006 including the expensive reason simplification developed in MiniSAT 1.14 (MiniLearningHeapExpSimp) * New command line configuration of solvers * Optional more robust (but less efficient) CNF input (allows to include comments between constraints): jar -jar sat4j.jar EZCNF:/my/dimacs/file.cnf * Basic support for And Inverter Graph format, in both ASCII (aag) and binary (aig) form. * Improved and simplified Pseudo Boolean code. * Fine code tuning provided by Dieter von Holten: 10% speedup in average. * Memory management: constraints are removed only when memory is exhausted. * Bug fixing in the optimization framework. * Improved code for the CSP to SAT conversion. * Improved Javadoc. * Rapid Restart Strategy, as in RSAT and picosat. * Improved solvers for pseudo boolean constraints * Use now Java generics to prevent user to setup a solver with incompatible components (i.e. a heuristics that needs information available only from a specific representation of binary clauses with a usual clause representation for instance). For more details, see https://wiki.objectweb.org/sat4j/Wiki.jsp?page=WhatsNewInSAT4J1.7 The release is available as 3 archives: * Full archive (sat4j-1.7.jar, 1.3MB) with all needed Java required libraries, including the Rhino Javascript interpreter needed by the CSP to SAT translator. * SAT friendly archive (sat4j-1.7-nojs.jar, 600 KB) without the Rhino library. It means that the CSP to SAT translator won't work out of the box (adding the rhino library to Java classpath fix the problem). This is the best option for people willing to have a simple way to try SAT4J for SAT solving. * Integrators friendly archive (sat4j-1.7-nojs-nocommons.jar, 348 KB) without the rhino nor the jakarta commons libraries needed by SAT4J (cli,beanutils and logging).             Date: 26-Nov-2006 Title: Special issue of JSAT on CFV Hits: 2112 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: 12-Oct-2006 Title: SAT 2007 Call For Paper: deadline for submission is January 19, 2007 Hits: 1529 Contributed by: Daniel Le Berre Keywords: Deduction Rules, BMC, DPLL, DP, Minimal models, Intelligent Backtracking, Data structure, Quasigroups, Local Search, Random 3SAT, Complexity, Randomization, Verification, Alternative approach, QBF, Structure of problems, Benchmark, SAT application, Randomised Algorithms, Randomised Problem Generation, Instance simplification, Learning, Model Elimination, SAT tools, branching heuristics, pseudo boolean optimization, variable ordering heuristic, preprocessors, MAXSAT, Preprocessing, Unit Propagation, symmetry, General Interest, call for papers, SAT-Based, Lookahead, Stochastic Satisfiability, SAT-Solver Competition, SAT/CP         SAT 2007 Call for Papers 10th International Conference on Theory and Applications of Satisfiability Testing May 28 - 31, Lisbon, Portugal http://sat07.ecs.soton.ac.uk The International Conference on Theory and Applications of Satisfiability Testing is the primary annual meeting for researchers studying the propositional satisfiability problem (SAT). SAT'07 is the tenth SAT conference. SAT'07 features the SAT competition, the QBF competition, the Pseudo-Boolean evaluation, and the MAX-SAT evaluation. SCOPE Many hard combinatorial problems can be encoded into SAT. Therefore improvements on heuristics on the practical, as well as theoretical insights into SAT apply to a large range of real-world problems. More specifically, many important practical verification problems can be rephrased as SAT problems. This applies to verification problems in hardware and software. Thus SAT is becoming one of the most important core technologies to verify secure and dependable systems. The topics of the conference span practical and theoretical research on SAT and its applications and include but are not limited to proof systems, proof complexity, search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, simplifiers, tools, case studies and empirical results. SAT is interpreted in a rather broad sense: besides propositional satisfiability, it includes the domain of quantified boolean formulae (QBF), constraints programming techniques (CSP) for word-level problems and their propositional encoding and particularly satisfiability modulo theories (SMT). SUBMISSION Submissions should contain original material and can either be regular research papers up to 14 pages or short papers up to 6 pages. Double submissions including submissions as short and long papers will be rejected. Submissions should use the Springer LNCS style. All appendices, tables, figures and the bibliography must fit into the page limit. Submissions deviating from these requirements may be rejected without review. All accepted papers including short papers will be published in the proceedings of the conference. The conference proceedings will be published within Springer LNCS series. The submission page is http://www.easychair.org/SAT2007. Papers have to be submitted electronically as PDF files. Paper submissions are due by January 19. PROGRAM CHAIRS Joao Marques-Silva, University of Southampton, UK Karem Sakallah, University of Michigan, USA LOCAL CHAIR Ines Lynce, Technical University of Lisbon, Portugal IMPORTANT DATES January 19, Paper Submission March 2, Author Notification March 16, Final Version More information on the conference web site.             Date: 16-May-2006 Title: 8th International Workshop on Preferences and Soft Constraints Hits: 1257 Contributed by: Cyril Terrioux Keywords: MAXSAT, General Interest         September 25th 2006, Nantes, France The interest of the community on preferences and soft constraints has increased in the last years. Examples are, from the modeling side, an active research on CP nets and some preference-based logic, and from the algorithmic side, several studies dealing with specific semantics of soft constraints such as propositional logic formulae (i.e. MAX-SAT) or global soft constraints in Constraint Programming or probability distributions (i.e. probabilistic reasoning) or uncertainty. The purpose of this workshop is to bring together researchers and practitioners who are interested in all aspects of preferences and soft constraints, such as: * theoretical frameworks * problem modeling * solving algorithms * decomposition methods and associated graph algorithms * tractability * languages * preference aggregation * preference elicitation * multi-objective or qualitative optimization * combining/integrating different frameworks and algorithms * comparative studies * real-life applications This year, the workshop is more specifically oriented towards graph decomposition approaches and tractability. Papers presenting new decomposition approaches, original criteria for selecting a decomposition, algorithms for generating interesting decompositions, comparison with existing approaches, theoretical and practical issues on the exploitation of such decompositions, new tractable classes... are especially welcome. Important Dates: * Paper Submission deadline: July 2nd * Notification of acceptance: July 22th * Workshop Date: September 25th             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: 13-Mar-2006 Title: First Evaluation of Max-SAT Solvers (MaxSAT-2006) Hits: 1624 Contributed by: Daniel Le Berre Keywords: MAXSAT, SAT-Solver Competition         First Evaluation of Max-SAT Solvers (MaxSAT-2006) The First Evaluation of Max-SAT Solvers (MaxSAT-2006) is organized as an affiliated event of the Ninth International Conference on Theory and Applications of Satisfiability Testing (SAT-2006). The objective of the evaluation is assessing the state of the art in the field of Max-SAT solvers, as well as creating a collection of publicly available Max-SAT benchmark instances. Important dates Submission of benchmarks April 3rd, 2006 First submission of solvers April 3rd, 2006 Testing and bug fixing April 10th-30th, 2006 Submission of definitive solvers May 5th, 2006 Experimentation May-June-July, 2006 Results of the evaluation August 12th-15th, 2006 Benchmarks and Solvers In the first evaluation we will focus the attention on exact solvers and unweighted Max-SAT instances. We plan to allow non-exact solvers and weighted instances in future evaluations. Benchmark instances should be submitted in DIMACS CNF format, and submitted solvers should be able to read that format (see the solver requirements). Submissions should be sent by e-mail to maxsat06@iiia.csic.es. The benchmarks used in the evaluation will be selected among the instances submitted and will not be published in advance. Nevertheless, a set of similar benchmark instances will be made available for testing purposes. Experimentation Only one version of the same solver will be accepted. For each instance and solver there will be a time limit between 15 and 30 minutes, depending on the number of submitted solvers. Assessment of solvers will be based on the number of successfully solved instances and the time needed to solve them. Solvers will run on machines with the following specification: * Operating System: Rocks Cluster 4.0.0 Linux 2.6.9 * Processor: AMD Opteron 248 Processor, 2 GHz * Memory: 2 GB * Cache: 1024 KB * Compilers: GCC 3.4.3, javac JDK 1.5.0 Organizing Committee Josep Argelich, University of Lleida, Spain Chu Min Li, University of Picardie, France Felip Manya, IIIA-CSIC, Spain Jordi Planes, University of Lleida, Spain To reach the organizers, send an e-mail to maxsat06@iiia.csic.es             Date: 21-Feb-2006 Title: Solving X3SAT Using Bipartite Graphs Hits: 1575 Contributed by: Russell A Easterly Keywords: Deduction Rules, Structure of problems, Instance simplification, MAXSAT, General Interest, X3SAT         I describe a method to solve certain classes of exclusive 3-SAT (X3SAT), also called exactly 1 in 3 SAT. The method is theoretically interesting because it doesn't use resolution. Instead, it finds bipartite subgraphs contained in certain types of graphs. The method has a worst case of O( n * 2^(m-1) ) where m is the number of clauses. Despite this, the method can quickly find solutions to many X3SAT instances. For example, this method will quickly solve instances that have many solutions. The method can also find all solutions to an instance. Many methods of solving X3SAT require detailed case by case analysis. This method is mechanically simple. It spends most of its time finding edges contained in subsets of vertices.             Date: 21-Jan-2006 Title: Boolean Functions - Theory, Algorithms, and Applications Hits: 2257 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: 16-Aug-2005 Title: Dynamic Symmetry-Breaking for Improved Boolean Optimization Hits: 2170 Contributed by:       Date: 08-Oct-2004 Title: Call for Papers for the Journal on Satisfiability, Boolean Modeling and Computation (JSAT) Hits: 2667 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: 28-Jul-2004 Title: UBCSAT version 1.0.0 available for download Hits: 2125 Contributed by: Dave Tompkins Keywords: Local Search, SAT tools, programming language, MAXSAT         The UBCSAT software is availabe for download at: http://www.satlib.org/ubcsat -- the software was described in a paper presented at SAT 2004. UBCSAT is a framework for Stochastic Local Search (SLS) algorithms for SAT. It includes fast implementations of many existing SLS algorithms (WalkSAT, SAPS, Adaptive Novelty+, ...) in a framework designed to facilitate the empirical analysis of SLS algorithms. UBCSAT has been designed to make it easy to add new algorithms and reporting capabilities, and so future releases will include more algorithms and features. Note that UBCSAT also provides support for the weighted MAX-SAT problem. If you would like to be notified of future releases of UBCSAT, we have set up a mailing list you can subscribe to (details are on the website).             Date: 23-Mar-2004 Title: SAT 2004 accepted papers Hits: 2767 Contributed by: Daniel Le Berre Keywords: Deduction Rules, BMC, DPLL, Minimal models, Intelligent Backtracking, Data structure, Quasigroups, Local Search, Repository, Random 3SAT, Complexity, Randomization, 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, branching heuristics, phase transition, binary clause reasoning, pseudo boolean optimization, variable ordering heuristic, MAXSAT, symmetry         Here is a list with abstracts of SAT2004 accepted papers. Note that the early registration fee apply up to March 24, that is tomorrow.             Date: 15-Jul-2003 Title: Solving Max-SAT as weighted CSP, Simon de Givry, J. Larrosa,P. Meseguer and T. Schiex In proc. of CP'2003, Cork (Ireland), Octobre 2003. Hits: 2416 Contributed by: Daniel Le Berre Keywords: SAT application, CSP, Linear Programming, pseudo boolean optimization, MAXSAT         The authors present an interesting comparison between pseudo boolean solvers such as OPBDP or PBS, mixed integer programming (Ilog CPLEX), Weighted CSP and dedicated solvers for solving MAX-SAT.             Date: 23-Jun-2003 Title: Iterated Robust Tabu Search for MAX-SAT. Kevin Smyth, Holger H. Hoos, and Thomas Stüutzle. Proc. of the Sixteenth Canadian Conference on Artificial Intelligence (AI'2003), 2003 (to appear). Hits: 1896 Contributed by: Daniel Le Berre Keywords: Local Search, MAXSAT           © 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.